Theorem rgen2 3197

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3062

This theorem is referenced by:  rgen3  3202  invdisjrabw  5133  invdisjrab  5134  sosn  5762  isoid  7325  f1owe  7349  epweon  7761  epweonALT  7762  f1stres  7998  f2ndres  7999  fnwelem  8116  soseq  8144  issmo  8347  oawordeulem  8553  naddf  8679  ecopover  8814  unfilem2  9310  dffi2  9417  inficl  9419  fipwuni  9420  fisn  9421  dffi3  9425  cantnfvalf  9659  r111  9769  alephf1  10079  alephiso  10092  dfac5lem4  10120  kmlem9  10152  ackbij1lem17  10230  fin1a2lem2  10395  fin1a2lem4  10397  axcc2lem  10430  smobeth  10580  nqereu  10923  addpqf  10938  mulpqf  10940  genpdm  10996  axaddf  11139  axmulf  11140  subf  11461  mulnzcnopr  11859  negiso  12193  cnref1o  12968  xaddf  13202  xmulf  13250  ioof  13423  om2uzf1oi  13917  om2uzisoi  13918  wrd2ind  14672  wwlktovf1  14907  reeff1  16062  divalglem9  16343  bitsf1  16386  smupf  16418  gcdf  16452  eucalgf  16519  qredeu  16594  1arith  16859  vdwapf  16904  xpsff1o  17512  catideu  17618  sscres  17769  fpwipodrs  18492  letsr  18545  mgmidmo  18578  frmdplusg  18734  efmndmgm  18765  smndex1mgm  18787  pwmnd  18817  mulgfval  18951  nmznsg  19047  efgmf  19580  efglem  19583  efgred  19615  isabli  19663  brric  20282  xrsmgm  20979  xrs1cmn  20984  xrge0subm  20985  xrsds  20987  cnsubmlem  20992  cnsubrglem  20994  nn0srg  21014  rge0srg  21015  rzgrp  21175  fibas  22479  fctop  22506  cctop  22508  iccordt  22717  txuni2  23068  fsubbas  23370  zfbas  23399  ismeti  23830  dscmet  24080  qtopbaslem  24274  tgqioo  24315  xrsxmet  24324  xrsdsre  24325  retopconn  24344  iccconn  24345  divcn  24383  abscncf  24416  recncf  24417  imcncf  24418  cjcncf  24419  iimulcn  24453  icopnfhmeo  24458  iccpnfhmeo  24460  xrhmeo  24461  cnllycmp  24471  bndth  24473  iundisj2  25065  dyadf  25107  reefiso  25959  recosf1o  26043  cxpcn3  26253  sgmf  26646  2lgslem1b  26892  lrcut  27394  addsf  27463  negscut  27510  negsf1o  27525  mulscutlem  27584  tgjustf  27721  ercgrg  27765  2wspmdisj  29587  isabloi  29799  smcnlem  29945  cncph  30067  hvsubf  30263  hhip  30425  hhph  30426  helch  30491  hsn0elch  30496  hhssabloilem  30509  hhshsslem2  30516  shscli  30565  shintcli  30577  pjmf1  30964  idunop  31226  0cnop  31227  0cnfn  31228  idcnop  31229  idhmop  31230  0hmop  31231  adj0  31242  lnophsi  31249  lnopunii  31260  lnophmi  31266  nlelshi  31308  riesz4i  31311  cnlnadjlem6  31320  cnlnadjlem9  31323  adjcoi  31348  bra11  31356  pjhmopi  31394  iundisj2f  31816  iundisj2fi  32003  xrstos  32175  xrge0omnd  32224  reofld  32454  xrge0slmod  32458  iistmd  32877  cnre2csqima  32886  mndpluscn  32901  raddcn  32904  xrge0iifiso  32910  xrge0iifmhm  32914  xrge0pluscn  32915  cnzh  32945  rezh  32946  br2base  33263  sxbrsiga  33284  signswmnd  33563  cardpred  34088  nummin  34089  indispconn  34220  cnllysconn  34231  ioosconn  34233  rellysconn  34237  fmlaomn0  34376  gonan0  34378  goaln0  34379  gg-divcn  35158  gg-iimulcn  35164  fneref  35230  dnicn  35363  f1omptsnlem  36212  isbasisrelowl  36234  poimirlem27  36510  mblfinlem1  36520  mblfinlem2  36521  exidu1  36719  rngoideu  36766  isomliN  38104  idlaut  38962  resubf  41255  sn-subf  41302  mzpclall  41455  frmx  41642  frmy  41643  kelac2lem  41796  onsucf1o  42012  ontric3g  42263  clsk1indlem3  42784  icof  43908  natglobalincr  45581  sprsymrelf1  46154  fmtnof1  46193  prmdvdsfmtnof1  46245  uspgrsprf1  46515  plusfreseq  46532  nnsgrpmgm  46576  nnsgrp  46577  nn0mnd  46579  pzriprnglem5  46799  pzriprnglem8  46802  2zrngamgm  46827  2zrngmmgm  46834  2zrngnmrid  46838  ldepslinc  47180  rrx2xpref1o  47394  rrx2plordisom  47399