Theorem rgen2 3206

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081

This theorem is used by:  rgen3  3211  invdisjrab  5095  sosn  5746  isoid  7368  f1owe  7392  f1oweOLD  7393  epweon  7821  epweonALT  7822  f1stres  8059  f2ndres  8060  fnwelem  8180  soseq  8213  issmo  8394  oawordeulem  8600  naddf  8729  ecopover  8880  unfilem2  9336  dffi2  9452  inficl  9454  fipwuni  9455  fisn  9456  dffi3  9460  cantnfvalf  9703  r111  9819  alephf1  10203  alephiso  10216  dfac5lem4  10244  kmlem9  10276  ackbij1lem17  10352  fin1a2lem2  10518  fin1a2lem4  10520  axcc2lem  10553  smobeth  10710  nqereu  11053  addpqf  11068  mulpqf  11070  genpdm  11126  axaddf  11269  axmulf  11270  subf  11598  mulnzcnf  12002  negiso  12337  cnref1o  13153  xaddf  13394  xmulf  13442  ioof  13618  om2uzf1oi  14136  om2uzisoi  14137  wrd2ind  14914  wwlktovf1  15153  reeff1  16332  divalglem9  16615  bitsf1  16660  smupf  16692  gcdf  16728  eucalgf  16802  qredeu  16877  1arith  17149  vdwapf  17194  xpsff1o  17789  catideu  17899  sscres  18048  fpwipodrs  18764  letsr  18817  chninf  18859  mgmidmo  18888  frmdplusg  19100  efmndmgm  19131  smndex1mgm  19156  pwmnd  19193  mulgfval  19329  nmznsg  19428  efgmf  19978  efglem  19981  efgred  20013  isabli  20061  xrsmgm  21765  xrsds  21768  cnsubmlem  21773  cnsubrglem  21775  nn0srg  21797  rge0srg  21798  xrs1cmn  21802  xrge0subm  21803  xrge0omnd  21805  pzriprnglem5  21846  pzriprnglem8  21849  rzgrp  21984  fibas  23350  fctop  23377  cctop  23379  iccordt  23587  txuni2  23939  fsubbas  24241  zfbas  24270  ismeti  24699  dscmet  24946  qtopbaslem  25132  tgqioo  25174  xrsxmet  25184  xrsdsre  25185  retopconn  25204  iccconn  25205  divcn  25244  abscncf  25277  recncf  25278  imcncf  25279  cjcncf  25280  iimulcn  25314  icopnfhmeo  25319  iccpnfhmeo  25321  xrhmeo  25322  cnllycmp  25332  bndth  25334  iundisj2  25925  dyadf  25967  reefiso  26832  recosf1o  26920  cxpcn3  27133  sgmf  27529  2lgslem1b  27776  lrcut  28347  addsf  28425  negcut  28482  negsf1o  28497  subsf  28507  mulcutlem  28574  oniso  28714  bdayn0sf1o  28813  zsoring  28852  tgjustf  28992  ercgrg  29037  2wspmdisj  30995  isabloi  31210  smcnlem  31356  cncph  31478  hvsubf  31674  hhip  31836  hhph  31837  helch  31902  hsn0elch  31907  hhssabloilem  31920  hhshsslem2  31927  shscli  31976  shintcli  31988  pjmf1  32375  idunop  32637  0cnop  32638  0cnfn  32639  idcnop  32640  idhmop  32641  0hmop  32642  adj0  32653  lnophsi  32660  lnopunii  32671  lnophmi  32677  nlelshi  32719  riesz4i  32722  cnlnadjlem6  32731  cnlnadjlem9  32734  adjcoi  32759  bra11  32767  pjhmopi  32805  iundisj2f  33282  iundisj2fi  33485  xrstos  33670  zzedom  33958  reofld  34008  xrge0slmod  34013  zringfrac  34189  iistmd  34645  cnre2csqima  34654  mndpluscn  34669  raddcn  34672  xrge0iifiso  34678  xrge0iifmhm  34682  xrge0pluscn  34683  cnzh  34711  rezh  34712  br2base  35012  sxbrsiga  35033  signswmnd  35297  cardpred  35846  nummin  35847  jf1  36051  indispconn  36207  cnllysconn  36218  ioosconn  36220  rellysconn  36224  fmlaomn0  36363  gonan0  36365  goaln0  36366  mpomulnzcnf  37303  fneref  37353  dnicn  37573  f1omptsnlem  38527  isbasisrelowl  38549  poimirlem27  38833  mblfinlem1  38843  mblfinlem2  38844  exidu1  39056  rngoideu  39103  isomliN  40562  idlaut  41419  resubf  43698  sn-subf  43746  mzpclall  44004  frmx  44186  frmy  44187  kelac2lem  44332  onsucf1o  44535  ontric3g  44784  clsk1indlem3  45304  wfaxpr  46252  hashomiso  46279  hfstructwe  46303  icof  46505  sprsymrelf1  48851  fmtnof1  48893  prmdvdsfmtnof1  48945  usgrexmpl2trifr  49408  uspgrsprf1  49518  plusfreseq  49534  nnsgrpmgm  49546  nnsgrp  49547  nn0mnd  49549  2zrngamgm  49615  2zrngmmgm  49622  2zrngnmrid  49626  subrgccdom  49709  ldepslinc  49952  rrx2plordisom  50167  rescofuf  50539  oppff1  50595