Theorem rgen2 3198

Description: Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3368 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 3147	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)
3	2	rgen 3064	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  rgen3  3203  invdisjrabw  5134  invdisjrab  5135  sosn  5763  isoid  7326  f1owe  7350  epweon  7762  epweonALT  7763  f1stres  7999  f2ndres  8000  fnwelem  8117  soseq  8145  issmo  8348  oawordeulem  8554  naddf  8680  ecopover  8815  unfilem2  9311  dffi2  9418  inficl  9420  fipwuni  9421  fisn  9422  dffi3  9426  cantnfvalf  9660  r111  9770  alephf1  10080  alephiso  10093  dfac5lem4  10121  kmlem9  10153  ackbij1lem17  10231  fin1a2lem2  10396  fin1a2lem4  10398  axcc2lem  10431  smobeth  10581  nqereu  10924  addpqf  10939  mulpqf  10941  genpdm  10997  axaddf  11140  axmulf  11141  subf  11462  mulnzcnopr  11860  negiso  12194  cnref1o  12969  xaddf  13203  xmulf  13251  ioof  13424  om2uzf1oi  13918  om2uzisoi  13919  wrd2ind  14673  wwlktovf1  14908  reeff1  16063  divalglem9  16344  bitsf1  16387  smupf  16419  gcdf  16453  eucalgf  16520  qredeu  16595  1arith  16860  vdwapf  16905  xpsff1o  17513  catideu  17619  sscres  17770  fpwipodrs  18493  letsr  18546  mgmidmo  18579  frmdplusg  18735  efmndmgm  18766  smndex1mgm  18788  pwmnd  18818  mulgfval  18952  nmznsg  19048  efgmf  19581  efglem  19584  efgred  19616  isabli  19664  brric  20283  xrsmgm  20980  xrs1cmn  20985  xrge0subm  20986  xrsds  20988  cnsubmlem  20993  cnsubrglem  20995  nn0srg  21015  rge0srg  21016  rzgrp  21176  fibas  22480  fctop  22507  cctop  22509  iccordt  22718  txuni2  23069  fsubbas  23371  zfbas  23400  ismeti  23831  dscmet  24081  qtopbaslem  24275  tgqioo  24316  xrsxmet  24325  xrsdsre  24326  retopconn  24345  iccconn  24346  divcn  24384  abscncf  24417  recncf  24418  imcncf  24419  cjcncf  24420  iimulcn  24454  icopnfhmeo  24459  iccpnfhmeo  24461  xrhmeo  24462  cnllycmp  24472  bndth  24474  iundisj2  25066  dyadf  25108  reefiso  25960  recosf1o  26044  cxpcn3  26256  sgmf  26649  2lgslem1b  26895  lrcut  27397  addsf  27466  negscut  27513  negsf1o  27528  mulscutlem  27587  tgjustf  27724  ercgrg  27768  2wspmdisj  29590  isabloi  29804  smcnlem  29950  cncph  30072  hvsubf  30268  hhip  30430  hhph  30431  helch  30496  hsn0elch  30501  hhssabloilem  30514  hhshsslem2  30521  shscli  30570  shintcli  30582  pjmf1  30969  idunop  31231  0cnop  31232  0cnfn  31233  idcnop  31234  idhmop  31235  0hmop  31236  adj0  31247  lnophsi  31254  lnopunii  31265  lnophmi  31271  nlelshi  31313  riesz4i  31316  cnlnadjlem6  31325  cnlnadjlem9  31328  adjcoi  31353  bra11  31361  pjhmopi  31399  iundisj2f  31821  iundisj2fi  32008  xrstos  32180  xrge0omnd  32229  reofld  32459  xrge0slmod  32463  iistmd  32882  cnre2csqima  32891  mndpluscn  32906  raddcn  32909  xrge0iifiso  32915  xrge0iifmhm  32919  xrge0pluscn  32920  cnzh  32950  rezh  32951  br2base  33268  sxbrsiga  33289  signswmnd  33568  cardpred  34093  nummin  34094  indispconn  34225  cnllysconn  34236  ioosconn  34238  rellysconn  34242  fmlaomn0  34381  gonan0  34383  goaln0  34384  gg-divcn  35163  gg-iimulcn  35169  fneref  35235  dnicn  35368  f1omptsnlem  36217  isbasisrelowl  36239  poimirlem27  36515  mblfinlem1  36525  mblfinlem2  36526  exidu1  36724  rngoideu  36771  isomliN  38109  idlaut  38967  resubf  41254  sn-subf  41301  mzpclall  41465  frmx  41652  frmy  41653  kelac2lem  41806  onsucf1o  42022  ontric3g  42273  clsk1indlem3  42794  icof  43918  natglobalincr  45591  sprsymrelf1  46164  fmtnof1  46203  prmdvdsfmtnof1  46255  uspgrsprf1  46525  plusfreseq  46542  nnsgrpmgm  46586  nnsgrp  46587  nn0mnd  46589  pzriprnglem5  46809  pzriprnglem8  46812  2zrngamgm  46837  2zrngmmgm  46844  2zrngnmrid  46848  ldepslinc  47190  rrx2xpref1o  47404  rrx2plordisom  47409