Theorem rgen2 3172

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  rgen3  3177  invdisjrab  5073  sosn  5698  isoid  7258  f1owe  7282  epweon  7703  epweonALT  7704  f1stres  7940  f2ndres  7941  fnwelem  8056  soseq  8084  issmo  8263  oawordeulem  8464  naddf  8591  ecopover  8740  unfilem2  9185  dffi2  9302  inficl  9304  fipwuni  9305  fisn  9306  dffi3  9310  cantnfvalf  9550  r111  9663  alephf1  9971  alephiso  9984  dfac5lem4  10012  dfac5lem4OLD  10014  kmlem9  10045  ackbij1lem17  10121  fin1a2lem2  10287  fin1a2lem4  10289  axcc2lem  10322  smobeth  10472  nqereu  10815  addpqf  10830  mulpqf  10832  genpdm  10888  axaddf  11031  axmulf  11032  subf  11357  mulnzcnf  11758  negiso  12097  cnref1o  12878  xaddf  13118  xmulf  13166  ioof  13342  om2uzf1oi  13855  om2uzisoi  13856  wrd2ind  14625  wwlktovf1  14859  reeff1  16024  divalglem9  16307  bitsf1  16352  smupf  16384  gcdf  16418  eucalgf  16489  qredeu  16564  1arith  16834  vdwapf  16879  xpsff1o  17466  catideu  17576  sscres  17725  fpwipodrs  18441  letsr  18494  chninf  18536  mgmidmo  18563  frmdplusg  18757  efmndmgm  18788  smndex1mgm  18810  pwmnd  18840  mulgfval  18977  nmznsg  19075  efgmf  19620  efglem  19623  efgred  19655  isabli  19703  brric  20414  xrsmgm  21338  xrsds  21341  cnsubmlem  21346  cnsubrglem  21348  cnsubrglemOLD  21349  nn0srg  21369  rge0srg  21370  xrs1cmn  21374  xrge0subm  21375  xrge0omnd  21377  pzriprnglem5  21417  pzriprnglem8  21420  rzgrp  21555  fibas  22887  fctop  22914  cctop  22916  iccordt  23124  txuni2  23475  fsubbas  23777  zfbas  23806  ismeti  24235  dscmet  24482  qtopbaslem  24668  tgqioo  24710  xrsxmet  24720  xrsdsre  24721  retopconn  24740  iccconn  24741  divcnOLD  24779  divcn  24781  abscncf  24816  recncf  24817  imcncf  24818  cjcncf  24819  iimulcn  24856  iimulcnOLD  24857  icopnfhmeo  24863  iccpnfhmeo  24865  xrhmeo  24866  cnllycmp  24877  bndth  24879  iundisj2  25472  dyadf  25514  reefiso  26380  recosf1o  26466  cxpcn3  26680  sgmf  27077  2lgslem1b  27325  lrcut  27844  addsf  27920  negscut  27976  negsf1o  27991  subsf  27999  mulscutlem  28065  onsiso  28200  bdayn0sf1o  28290  zsoring  28327  tgjustf  28446  ercgrg  28490  2wspmdisj  30309  isabloi  30523  smcnlem  30669  cncph  30791  hvsubf  30987  hhip  31149  hhph  31150  helch  31215  hsn0elch  31220  hhssabloilem  31233  hhshsslem2  31240  shscli  31289  shintcli  31301  pjmf1  31688  idunop  31950  0cnop  31951  0cnfn  31952  idcnop  31953  idhmop  31954  0hmop  31955  adj0  31966  lnophsi  31973  lnopunii  31984  lnophmi  31990  nlelshi  32032  riesz4i  32035  cnlnadjlem6  32044  cnlnadjlem9  32047  adjcoi  32072  bra11  32080  pjhmopi  32118  iundisj2f  32562  iundisj2fi  32771  xrstos  32983  reofld  33300  xrge0slmod  33305  zringfrac  33511  iistmd  33907  cnre2csqima  33916  mndpluscn  33931  raddcn  33934  xrge0iifiso  33940  xrge0iifmhm  33944  xrge0pluscn  33945  cnzh  33973  rezh  33974  br2base  34274  sxbrsiga  34295  signswmnd  34562  cardpred  35095  nummin  35096  indispconn  35270  cnllysconn  35281  ioosconn  35283  rellysconn  35287  fmlaomn0  35426  gonan0  35428  goaln0  35429  mpomulnzcnf  36333  fneref  36384  dnicn  36526  f1omptsnlem  37370  isbasisrelowl  37392  poimirlem27  37687  mblfinlem1  37697  mblfinlem2  37698  exidu1  37896  rngoideu  37943  isomliN  39278  idlaut  40135  resubf  42414  sn-subf  42462  mzpclall  42760  frmx  42946  frmy  42947  kelac2lem  43097  onsucf1o  43305  ontric3g  43555  clsk1indlem3  44076  wfaxpr  45031  icof  45256  natglobalincr  46915  sprsymrelf1  47527  fmtnof1  47566  prmdvdsfmtnof1  47618  usgrexmpl2trifr  48068  uspgrsprf1  48178  plusfreseq  48195  nnsgrpmgm  48207  nnsgrp  48208  nn0mnd  48210  2zrngamgm  48276  2zrngmmgm  48283  2zrngnmrid  48287  ldepslinc  48541  rrx2xpref1o  48750  rrx2plordisom  48755  rescofuf  49125  oppff1  49180