Theorem rgen2 3211

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 3163	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)
3	2	rgen 3087	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  rgen3  3216  invdisjrab  5097  sosn  5746  isoid  7325  f1owe  7349  epweon  7770  epweonALT  7771  f1stres  8006  f2ndres  8007  fnwelem  8123  soseq  8151  issmo  8331  oawordeulem  8535  naddf  8664  ecopover  8815  unfilem2  9262  dffi2  9379  inficl  9381  fipwuni  9382  fisn  9383  dffi3  9387  cantnfvalf  9630  r111  9743  alephf1  10065  alephiso  10078  dfac5lem4  10106  kmlem9  10138  ackbij1lem17  10214  fin1a2lem2  10381  fin1a2lem4  10383  axcc2lem  10416  smobeth  10567  nqereu  10910  addpqf  10925  mulpqf  10927  genpdm  10983  axaddf  11126  axmulf  11127  subf  11455  mulnzcnf  11856  negiso  12191  cnref1o  13005  xaddf  13246  xmulf  13294  ioof  13470  om2uzf1oi  13985  om2uzisoi  13986  wrd2ind  14756  wwlktovf1  14990  reeff1  16172  divalglem9  16455  bitsf1  16500  smupf  16532  gcdf  16566  eucalgf  16637  qredeu  16712  1arith  16983  vdwapf  17028  xpsff1o  17617  catideu  17727  sscres  17876  fpwipodrs  18592  letsr  18645  chninf  18687  mgmidmo  18714  frmdplusg  18909  efmndmgm  18940  smndex1mgm  18965  pwmnd  18995  mulgfval  19131  nmznsg  19230  efgmf  19779  efglem  19782  efgred  19814  isabli  19862  brric  20582  xrsmgm  21522  xrsds  21525  cnsubmlem  21530  cnsubrglem  21532  nn0srg  21552  rge0srg  21553  xrs1cmn  21557  xrge0subm  21558  xrge0omnd  21560  pzriprnglem5  21600  pzriprnglem8  21603  rzgrp  21738  fibas  23099  fctop  23126  cctop  23128  iccordt  23336  txuni2  23687  fsubbas  23989  zfbas  24018  ismeti  24447  dscmet  24694  qtopbaslem  24880  tgqioo  24922  xrsxmet  24932  xrsdsre  24933  retopconn  24952  iccconn  24953  divcn  24992  abscncf  25025  recncf  25026  imcncf  25027  cjcncf  25028  iimulcn  25062  icopnfhmeo  25067  iccpnfhmeo  25069  xrhmeo  25070  cnllycmp  25080  bndth  25082  iundisj2  25673  dyadf  25715  reefiso  26573  recosf1o  26662  cxpcn3  26875  sgmf  27271  2lgslem1b  27518  lrcut  28059  addsf  28137  negcut  28194  negsf1o  28209  subsf  28219  mulcutlem  28286  oniso  28426  bdayn0sf1o  28525  zsoring  28564  tgjustf  28704  ercgrg  28748  2wspmdisj  30625  isabloi  30840  smcnlem  30986  cncph  31108  hvsubf  31304  hhip  31466  hhph  31467  helch  31532  hsn0elch  31537  hhssabloilem  31550  hhshsslem2  31557  shscli  31606  shintcli  31618  pjmf1  32005  idunop  32267  0cnop  32268  0cnfn  32269  idcnop  32270  idhmop  32271  0hmop  32272  adj0  32283  lnophsi  32290  lnopunii  32301  lnophmi  32307  nlelshi  32349  riesz4i  32352  cnlnadjlem6  32361  cnlnadjlem9  32364  adjcoi  32389  bra11  32397  pjhmopi  32435  iundisj2f  32872  iundisj2fi  33079  xrstos  33267  reofld  33602  xrge0slmod  33607  zringfrac  33785  iistmd  34233  cnre2csqima  34242  mndpluscn  34257  raddcn  34260  xrge0iifiso  34266  xrge0iifmhm  34270  xrge0pluscn  34271  cnzh  34299  rezh  34300  br2base  34600  sxbrsiga  34621  signswmnd  34885  cardpred  35422  nummin  35423  indispconn  35621  cnllysconn  35632  ioosconn  35634  rellysconn  35638  fmlaomn0  35777  gonan0  35779  goaln0  35780  mpomulnzcnf  36696  fneref  36746  dnicn  36966  f1omptsnlem  37865  isbasisrelowl  37887  poimirlem27  38181  mblfinlem1  38191  mblfinlem2  38192  exidu1  38390  rngoideu  38437  isomliN  39898  idlaut  40755  resubf  43027  sn-subf  43075  mzpclall  43345  frmx  43527  frmy  43528  kelac2lem  43678  onsucf1o  43886  ontric3g  44135  clsk1indlem3  44656  wfaxpr  45594  hashomiso  45621  icof  45822  natglobalincr  47480  sprsymrelf1  48129  fmtnof1  48171  prmdvdsfmtnof1  48223  usgrexmpl2trifr  48686  uspgrsprf1  48796  plusfreseq  48813  nnsgrpmgm  48825  nnsgrp  48826  nn0mnd  48828  2zrngamgm  48894  2zrngmmgm  48901  2zrngnmrid  48905  ldepslinc  49169  rrx2xpref1o  49378  rrx2plordisom  49383  rescofuf  49751  oppff1  49806