Theorem rgen2 3194

Description: Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3364 since it depends on a smaller set of axioms. (Contributed by NM, 30-May-1999.)

Hypothesis

Ref	Expression
rgen2.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)

Assertion

Ref	Expression
rgen2	⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rgen2

Step	Hyp	Ref	Expression
1		rgen2.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)
2	1	ralrimiva 3143	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)
3	2	rgen 3060	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3059

This theorem is referenced by:  rgen3  3199  invdisjrabw  5133  invdisjrab  5134  sosn  5764  isoid  7337  f1owe  7361  epweon  7777  epweonALT  7778  f1stres  8017  f2ndres  8018  fnwelem  8136  soseq  8164  issmo  8368  oawordeulem  8574  naddf  8701  ecopover  8839  unfilem2  9335  dffi2  9446  inficl  9448  fipwuni  9449  fisn  9450  dffi3  9454  cantnfvalf  9688  r111  9798  alephf1  10108  alephiso  10121  dfac5lem4  10149  kmlem9  10181  ackbij1lem17  10259  fin1a2lem2  10424  fin1a2lem4  10426  axcc2lem  10459  smobeth  10609  nqereu  10952  addpqf  10967  mulpqf  10969  genpdm  11025  axaddf  11168  axmulf  11169  subf  11492  mulnzcnf  11890  negiso  12224  cnref1o  12999  xaddf  13235  xmulf  13283  ioof  13456  om2uzf1oi  13950  om2uzisoi  13951  wrd2ind  14705  wwlktovf1  14940  reeff1  16096  divalglem9  16377  bitsf1  16420  smupf  16452  gcdf  16486  eucalgf  16553  qredeu  16628  1arith  16895  vdwapf  16940  xpsff1o  17548  catideu  17654  sscres  17805  fpwipodrs  18531  letsr  18584  mgmidmo  18619  frmdplusg  18805  efmndmgm  18836  smndex1mgm  18858  pwmnd  18888  mulgfval  19024  nmznsg  19122  efgmf  19667  efglem  19670  efgred  19702  isabli  19750  brric  20442  xrsmgm  21333  xrs1cmn  21338  xrge0subm  21339  xrsds  21341  cnsubmlem  21346  cnsubrglem  21348  cnsubrglemOLD  21349  nn0srg  21369  rge0srg  21370  pzriprnglem5  21410  pzriprnglem8  21413  rzgrp  21554  fibas  22879  fctop  22906  cctop  22908  iccordt  23117  txuni2  23468  fsubbas  23770  zfbas  23799  ismeti  24230  dscmet  24480  qtopbaslem  24674  tgqioo  24715  xrsxmet  24724  xrsdsre  24725  retopconn  24744  iccconn  24745  divcnOLD  24783  divcn  24785  abscncf  24820  recncf  24821  imcncf  24822  cjcncf  24823  iimulcn  24860  iimulcnOLD  24861  icopnfhmeo  24867  iccpnfhmeo  24869  xrhmeo  24870  cnllycmp  24881  bndth  24883  iundisj2  25477  dyadf  25519  reefiso  26384  recosf1o  26468  cxpcn3  26682  sgmf  27076  2lgslem1b  27324  lrcut  27828  addsf  27898  negscut  27950  negsf1o  27965  mulscutlem  28030  tgjustf  28276  ercgrg  28320  2wspmdisj  30146  isabloi  30360  smcnlem  30506  cncph  30628  hvsubf  30824  hhip  30986  hhph  30987  helch  31052  hsn0elch  31057  hhssabloilem  31070  hhshsslem2  31077  shscli  31126  shintcli  31138  pjmf1  31525  idunop  31787  0cnop  31788  0cnfn  31789  idcnop  31790  idhmop  31791  0hmop  31792  adj0  31803  lnophsi  31810  lnopunii  31821  lnophmi  31827  nlelshi  31869  riesz4i  31872  cnlnadjlem6  31881  cnlnadjlem9  31884  adjcoi  31909  bra11  31917  pjhmopi  31955  iundisj2f  32379  iundisj2fi  32565  xrstos  32737  xrge0omnd  32791  zringfrac  32996  reofld  33056  xrge0slmod  33060  iistmd  33503  cnre2csqima  33512  mndpluscn  33527  raddcn  33530  xrge0iifiso  33536  xrge0iifmhm  33540  xrge0pluscn  33541  cnzh  33571  rezh  33572  br2base  33889  sxbrsiga  33910  signswmnd  34189  cardpred  34713  nummin  34714  indispconn  34844  cnllysconn  34855  ioosconn  34857  rellysconn  34861  fmlaomn0  35000  gonan0  35002  goaln0  35003  mpomulnzcnf  35783  fneref  35834  dnicn  35967  f1omptsnlem  36815  isbasisrelowl  36837  poimirlem27  37120  mblfinlem1  37130  mblfinlem2  37131  exidu1  37329  rngoideu  37376  isomliN  38711  idlaut  39569  resubf  41936  sn-subf  41983  mzpclall  42147  frmx  42334  frmy  42335  kelac2lem  42488  onsucf1o  42701  ontric3g  42952  clsk1indlem3  43473  icof  44592  natglobalincr  46263  sprsymrelf1  46836  fmtnof1  46875  prmdvdsfmtnof1  46927  uspgrsprf1  47209  plusfreseq  47226  nnsgrpmgm  47238  nnsgrp  47239  nn0mnd  47241  2zrngamgm  47307  2zrngmmgm  47314  2zrngnmrid  47318  ldepslinc  47577  rrx2xpref1o  47791  rrx2plordisom  47796

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »