Theorem rgen2 3173

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3048

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 3049

This theorem is referenced by:  rgen3  3178  invdisjrab  5082  sosn  5708  isoid  7272  f1owe  7296  epweon  7717  epweonALT  7718  f1stres  7954  f2ndres  7955  fnwelem  8070  soseq  8098  issmo  8277  oawordeulem  8478  naddf  8605  ecopover  8754  unfilem2  9201  dffi2  9318  inficl  9320  fipwuni  9321  fisn  9322  dffi3  9326  cantnfvalf  9566  r111  9679  alephf1  9987  alephiso  10000  dfac5lem4  10028  dfac5lem4OLD  10030  kmlem9  10061  ackbij1lem17  10137  fin1a2lem2  10303  fin1a2lem4  10305  axcc2lem  10338  smobeth  10488  nqereu  10831  addpqf  10846  mulpqf  10848  genpdm  10904  axaddf  11047  axmulf  11048  subf  11373  mulnzcnf  11774  negiso  12113  cnref1o  12889  xaddf  13130  xmulf  13178  ioof  13354  om2uzf1oi  13867  om2uzisoi  13868  wrd2ind  14637  wwlktovf1  14871  reeff1  16036  divalglem9  16319  bitsf1  16364  smupf  16396  gcdf  16430  eucalgf  16501  qredeu  16576  1arith  16846  vdwapf  16891  xpsff1o  17479  catideu  17589  sscres  17738  fpwipodrs  18454  letsr  18507  chninf  18549  mgmidmo  18576  frmdplusg  18770  efmndmgm  18801  smndex1mgm  18823  pwmnd  18853  mulgfval  18990  nmznsg  19088  efgmf  19633  efglem  19636  efgred  19668  isabli  19716  brric  20428  xrsmgm  21352  xrsds  21355  cnsubmlem  21360  cnsubrglem  21362  cnsubrglemOLD  21363  nn0srg  21383  rge0srg  21384  xrs1cmn  21388  xrge0subm  21389  xrge0omnd  21391  pzriprnglem5  21431  pzriprnglem8  21434  rzgrp  21569  fibas  22912  fctop  22939  cctop  22941  iccordt  23149  txuni2  23500  fsubbas  23802  zfbas  23831  ismeti  24260  dscmet  24507  qtopbaslem  24693  tgqioo  24735  xrsxmet  24745  xrsdsre  24746  retopconn  24765  iccconn  24766  divcnOLD  24804  divcn  24806  abscncf  24841  recncf  24842  imcncf  24843  cjcncf  24844  iimulcn  24881  iimulcnOLD  24882  icopnfhmeo  24888  iccpnfhmeo  24890  xrhmeo  24891  cnllycmp  24902  bndth  24904  iundisj2  25497  dyadf  25539  reefiso  26405  recosf1o  26491  cxpcn3  26705  sgmf  27102  2lgslem1b  27350  lrcut  27869  addsf  27945  negscut  28001  negsf1o  28016  subsf  28024  mulscutlem  28090  onsiso  28225  bdayn0sf1o  28315  zsoring  28352  tgjustf  28471  ercgrg  28515  2wspmdisj  30338  isabloi  30552  smcnlem  30698  cncph  30820  hvsubf  31016  hhip  31178  hhph  31179  helch  31244  hsn0elch  31249  hhssabloilem  31262  hhshsslem2  31269  shscli  31318  shintcli  31330  pjmf1  31717  idunop  31979  0cnop  31980  0cnfn  31981  idcnop  31982  idhmop  31983  0hmop  31984  adj0  31995  lnophsi  32002  lnopunii  32013  lnophmi  32019  nlelshi  32061  riesz4i  32064  cnlnadjlem6  32073  cnlnadjlem9  32076  adjcoi  32101  bra11  32109  pjhmopi  32147  iundisj2f  32591  iundisj2fi  32805  xrstos  33020  reofld  33352  xrge0slmod  33357  zringfrac  33563  iistmd  33987  cnre2csqima  33996  mndpluscn  34011  raddcn  34014  xrge0iifiso  34020  xrge0iifmhm  34024  xrge0pluscn  34025  cnzh  34053  rezh  34054  br2base  34354  sxbrsiga  34375  signswmnd  34642  cardpred  35175  nummin  35176  indispconn  35350  cnllysconn  35361  ioosconn  35363  rellysconn  35367  fmlaomn0  35506  gonan0  35508  goaln0  35509  mpomulnzcnf  36415  fneref  36466  dnicn  36608  f1omptsnlem  37453  isbasisrelowl  37475  poimirlem27  37760  mblfinlem1  37770  mblfinlem2  37771  exidu1  37969  rngoideu  38016  isomliN  39411  idlaut  40268  resubf  42551  sn-subf  42599  mzpclall  42884  frmx  43070  frmy  43071  kelac2lem  43221  onsucf1o  43429  ontric3g  43679  clsk1indlem3  44200  wfaxpr  45155  icof  45379  natglobalincr  47037  sprsymrelf1  47658  fmtnof1  47697  prmdvdsfmtnof1  47749  usgrexmpl2trifr  48199  uspgrsprf1  48309  plusfreseq  48326  nnsgrpmgm  48338  nnsgrp  48339  nn0mnd  48341  2zrngamgm  48407  2zrngmmgm  48414  2zrngnmrid  48418  ldepslinc  48671  rrx2xpref1o  48880  rrx2plordisom  48885  rescofuf  49254  oppff1  49309