Theorem rgen2 3175

Description: Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3342 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 3046	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

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

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 3045

This theorem is referenced by:  rgen3  3180  invdisjrab  5089  sosn  5718  isoid  7286  f1owe  7310  epweon  7731  epweonALT  7732  f1stres  7971  f2ndres  7972  fnwelem  8087  soseq  8115  issmo  8294  oawordeulem  8495  naddf  8622  ecopover  8771  unfilem2  9231  dffi2  9350  inficl  9352  fipwuni  9353  fisn  9354  dffi3  9358  cantnfvalf  9594  r111  9704  alephf1  10014  alephiso  10027  dfac5lem4  10055  dfac5lem4OLD  10057  kmlem9  10088  ackbij1lem17  10164  fin1a2lem2  10330  fin1a2lem4  10332  axcc2lem  10365  smobeth  10515  nqereu  10858  addpqf  10873  mulpqf  10875  genpdm  10931  axaddf  11074  axmulf  11075  subf  11399  mulnzcnf  11800  negiso  12139  cnref1o  12920  xaddf  13160  xmulf  13208  ioof  13384  om2uzf1oi  13894  om2uzisoi  13895  wrd2ind  14664  wwlktovf1  14899  reeff1  16064  divalglem9  16347  bitsf1  16392  smupf  16424  gcdf  16458  eucalgf  16529  qredeu  16604  1arith  16874  vdwapf  16919  xpsff1o  17506  catideu  17612  sscres  17761  fpwipodrs  18475  letsr  18528  mgmidmo  18563  frmdplusg  18757  efmndmgm  18788  smndex1mgm  18810  pwmnd  18840  mulgfval  18977  nmznsg  19076  efgmf  19619  efglem  19622  efgred  19654  isabli  19702  brric  20389  xrsmgm  21294  xrs1cmn  21299  xrge0subm  21300  xrsds  21302  cnsubmlem  21307  cnsubrglem  21309  cnsubrglemOLD  21310  nn0srg  21330  rge0srg  21331  pzriprnglem5  21371  pzriprnglem8  21374  rzgrp  21508  fibas  22840  fctop  22867  cctop  22869  iccordt  23077  txuni2  23428  fsubbas  23730  zfbas  23759  ismeti  24189  dscmet  24436  qtopbaslem  24622  tgqioo  24664  xrsxmet  24674  xrsdsre  24675  retopconn  24694  iccconn  24695  divcnOLD  24733  divcn  24735  abscncf  24770  recncf  24771  imcncf  24772  cjcncf  24773  iimulcn  24810  iimulcnOLD  24811  icopnfhmeo  24817  iccpnfhmeo  24819  xrhmeo  24820  cnllycmp  24831  bndth  24833  iundisj2  25426  dyadf  25468  reefiso  26334  recosf1o  26420  cxpcn3  26634  sgmf  27031  2lgslem1b  27279  lrcut  27791  addsf  27865  negscut  27921  negsf1o  27936  subsf  27944  mulscutlem  28010  onsiso  28145  bdayn0sf1o  28235  tgjustf  28376  ercgrg  28420  2wspmdisj  30239  isabloi  30453  smcnlem  30599  cncph  30721  hvsubf  30917  hhip  31079  hhph  31080  helch  31145  hsn0elch  31150  hhssabloilem  31163  hhshsslem2  31170  shscli  31219  shintcli  31231  pjmf1  31618  idunop  31880  0cnop  31881  0cnfn  31882  idcnop  31883  idhmop  31884  0hmop  31885  adj0  31896  lnophsi  31903  lnopunii  31914  lnophmi  31920  nlelshi  31962  riesz4i  31965  cnlnadjlem6  31974  cnlnadjlem9  31977  adjcoi  32002  bra11  32010  pjhmopi  32048  iundisj2f  32492  iundisj2fi  32693  xrstos  32921  xrge0omnd  32998  reofld  33288  xrge0slmod  33292  zringfrac  33498  iistmd  33865  cnre2csqima  33874  mndpluscn  33889  raddcn  33892  xrge0iifiso  33898  xrge0iifmhm  33902  xrge0pluscn  33903  cnzh  33931  rezh  33932  br2base  34233  sxbrsiga  34254  signswmnd  34521  cardpred  35053  nummin  35054  indispconn  35194  cnllysconn  35205  ioosconn  35207  rellysconn  35211  fmlaomn0  35350  gonan0  35352  goaln0  35353  mpomulnzcnf  36260  fneref  36311  dnicn  36453  f1omptsnlem  37297  isbasisrelowl  37319  poimirlem27  37614  mblfinlem1  37624  mblfinlem2  37625  exidu1  37823  rngoideu  37870  isomliN  39205  idlaut  40063  resubf  42342  sn-subf  42390  mzpclall  42688  frmx  42875  frmy  42876  kelac2lem  43026  onsucf1o  43234  ontric3g  43484  clsk1indlem3  44005  wfaxpr  44961  icof  45186  natglobalincr  46848  sprsymrelf1  47470  fmtnof1  47509  prmdvdsfmtnof1  47561  usgrexmpl2trifr  48001  uspgrsprf1  48108  plusfreseq  48125  nnsgrpmgm  48137  nnsgrp  48138  nn0mnd  48140  2zrngamgm  48206  2zrngmmgm  48213  2zrngnmrid  48217  ldepslinc  48471  rrx2xpref1o  48680  rrx2plordisom  48685  rescofuf  49055  oppff1  49110