Theorem rgen2 3185

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053

This theorem is referenced by:  rgen3  3190  invdisjrab  5111  sosn  5746  isoid  7327  f1owe  7351  epweon  7774  epweonALT  7775  f1stres  8017  f2ndres  8018  fnwelem  8135  soseq  8163  issmo  8367  oawordeulem  8571  naddf  8698  ecopover  8840  unfilem2  9321  dffi2  9440  inficl  9442  fipwuni  9443  fisn  9444  dffi3  9448  cantnfvalf  9684  r111  9794  alephf1  10104  alephiso  10117  dfac5lem4  10145  dfac5lem4OLD  10147  kmlem9  10178  ackbij1lem17  10254  fin1a2lem2  10420  fin1a2lem4  10422  axcc2lem  10455  smobeth  10605  nqereu  10948  addpqf  10963  mulpqf  10965  genpdm  11021  axaddf  11164  axmulf  11165  subf  11489  mulnzcnf  11888  negiso  12227  cnref1o  13006  xaddf  13245  xmulf  13293  ioof  13469  om2uzf1oi  13976  om2uzisoi  13977  wrd2ind  14746  wwlktovf1  14981  reeff1  16143  divalglem9  16425  bitsf1  16470  smupf  16502  gcdf  16536  eucalgf  16607  qredeu  16682  1arith  16952  vdwapf  16997  xpsff1o  17586  catideu  17692  sscres  17841  fpwipodrs  18555  letsr  18608  mgmidmo  18643  frmdplusg  18837  efmndmgm  18868  smndex1mgm  18890  pwmnd  18920  mulgfval  19057  nmznsg  19156  efgmf  19699  efglem  19702  efgred  19734  isabli  19782  brric  20469  xrsmgm  21374  xrs1cmn  21379  xrge0subm  21380  xrsds  21382  cnsubmlem  21387  cnsubrglem  21389  cnsubrglemOLD  21390  nn0srg  21410  rge0srg  21411  pzriprnglem5  21451  pzriprnglem8  21454  rzgrp  21588  fibas  22920  fctop  22947  cctop  22949  iccordt  23157  txuni2  23508  fsubbas  23810  zfbas  23839  ismeti  24269  dscmet  24516  qtopbaslem  24702  tgqioo  24744  xrsxmet  24754  xrsdsre  24755  retopconn  24774  iccconn  24775  divcnOLD  24813  divcn  24815  abscncf  24850  recncf  24851  imcncf  24852  cjcncf  24853  iimulcn  24890  iimulcnOLD  24891  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  cnllycmp  24911  bndth  24913  iundisj2  25507  dyadf  25549  reefiso  26415  recosf1o  26501  cxpcn3  26715  sgmf  27112  2lgslem1b  27360  lrcut  27872  addsf  27946  negscut  28002  negsf1o  28017  subsf  28025  mulscutlem  28091  onsiso  28226  bdayn0sf1o  28316  tgjustf  28457  ercgrg  28501  2wspmdisj  30323  isabloi  30537  smcnlem  30683  cncph  30805  hvsubf  31001  hhip  31163  hhph  31164  helch  31229  hsn0elch  31234  hhssabloilem  31247  hhshsslem2  31254  shscli  31303  shintcli  31315  pjmf1  31702  idunop  31964  0cnop  31965  0cnfn  31966  idcnop  31967  idhmop  31968  0hmop  31969  adj0  31980  lnophsi  31987  lnopunii  31998  lnophmi  32004  nlelshi  32046  riesz4i  32049  cnlnadjlem6  32058  cnlnadjlem9  32061  adjcoi  32086  bra11  32094  pjhmopi  32132  iundisj2f  32576  iundisj2fi  32779  xrstos  33007  xrge0omnd  33084  reofld  33364  xrge0slmod  33368  zringfrac  33574  iistmd  33938  cnre2csqima  33947  mndpluscn  33962  raddcn  33965  xrge0iifiso  33971  xrge0iifmhm  33975  xrge0pluscn  33976  cnzh  34004  rezh  34005  br2base  34306  sxbrsiga  34327  signswmnd  34594  cardpred  35126  nummin  35127  indispconn  35261  cnllysconn  35272  ioosconn  35274  rellysconn  35278  fmlaomn0  35417  gonan0  35419  goaln0  35420  mpomulnzcnf  36322  fneref  36373  dnicn  36515  f1omptsnlem  37359  isbasisrelowl  37381  poimirlem27  37676  mblfinlem1  37686  mblfinlem2  37687  exidu1  37885  rngoideu  37932  isomliN  39262  idlaut  40120  resubf  42399  sn-subf  42446  mzpclall  42725  frmx  42912  frmy  42913  kelac2lem  43063  onsucf1o  43271  ontric3g  43521  clsk1indlem3  44042  wfaxpr  44998  icof  45223  natglobalincr  46886  sprsymrelf1  47490  fmtnof1  47529  prmdvdsfmtnof1  47581  usgrexmpl2trifr  48021  uspgrsprf1  48102  plusfreseq  48119  nnsgrpmgm  48131  nnsgrp  48132  nn0mnd  48134  2zrngamgm  48200  2zrngmmgm  48207  2zrngnmrid  48211  ldepslinc  48465  rrx2xpref1o  48678  rrx2plordisom  48683  rescofuf  49036