Theorem rgen2 3168

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3106

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3111

This theorem is referenced by:  rgen3  3169  invdisjrabw  5015  invdisjrab  5016  sosn  5602  isoid  7061  f1owe  7085  epweon  7477  f1stres  7695  f2ndres  7696  fnwelem  7808  issmo  7968  oawordeulem  8163  ecopover  8384  unfilem2  8767  dffi2  8871  inficl  8873  fipwuni  8874  fisn  8875  dffi3  8879  cantnfvalf  9112  r111  9188  alephf1  9496  alephiso  9509  dfac5lem4  9537  kmlem9  9569  ackbij1lem17  9647  fin1a2lem2  9812  fin1a2lem4  9814  axcc2lem  9847  smobeth  9997  nqereu  10340  addpqf  10355  mulpqf  10357  genpdm  10413  axaddf  10556  axmulf  10557  subf  10877  mulnzcnopr  11275  negiso  11608  cnref1o  12372  xaddf  12605  xmulf  12653  ioof  12825  om2uzf1oi  13316  om2uzisoi  13317  wrd2ind  14076  wwlktovf1  14312  reeff1  15465  divalglem9  15742  bitsf1  15785  smupf  15817  gcdf  15851  eucalgf  15917  qredeu  15992  1arith  16253  vdwapf  16298  xpsff1o  16832  catideu  16938  sscres  17085  fpwipodrs  17766  letsr  17829  mgmidmo  17862  frmdplusg  18011  efmndmgm  18042  smndex1mgm  18064  pwmnd  18094  mulgfval  18218  nmznsg  18312  efgmf  18831  efglem  18834  efgred  18866  isabli  18913  brric  19492  xrsmgm  20126  xrs1cmn  20131  xrge0subm  20132  xrsds  20134  cnsubmlem  20139  cnsubrglem  20141  nn0srg  20161  rge0srg  20162  rzgrp  20312  fibas  21582  fctop  21609  cctop  21611  iccordt  21819  txuni2  22170  fsubbas  22472  zfbas  22501  ismeti  22932  dscmet  23179  qtopbaslem  23364  tgqioo  23405  xrsxmet  23414  xrsdsre  23415  retopconn  23434  iccconn  23435  divcn  23473  abscncf  23506  recncf  23507  imcncf  23508  cjcncf  23509  iimulcn  23543  icopnfhmeo  23548  iccpnfhmeo  23550  xrhmeo  23551  cnllycmp  23561  bndth  23563  iundisj2  24153  dyadf  24195  reefiso  25043  recosf1o  25127  cxpcn3  25337  sgmf  25730  2lgslem1b  25976  tgjustf  26267  ercgrg  26311  2wspmdisj  28122  isabloi  28334  smcnlem  28480  cncph  28602  hvsubf  28798  hhip  28960  hhph  28961  helch  29026  hsn0elch  29031  hhssabloilem  29044  hhshsslem2  29051  shscli  29100  shintcli  29112  pjmf1  29499  idunop  29761  0cnop  29762  0cnfn  29763  idcnop  29764  idhmop  29765  0hmop  29766  adj0  29777  lnophsi  29784  lnopunii  29795  lnophmi  29801  nlelshi  29843  riesz4i  29846  cnlnadjlem6  29855  cnlnadjlem9  29858  adjcoi  29883  bra11  29891  pjhmopi  29929  iundisj2f  30353  iundisj2fi  30546  xrstos  30713  xrge0omnd  30762  reofld  30964  xrge0slmod  30968  iistmd  31255  cnre2csqima  31264  mndpluscn  31279  raddcn  31282  xrge0iifiso  31288  xrge0iifmhm  31292  xrge0pluscn  31293  cnzh  31321  rezh  31322  br2base  31637  sxbrsiga  31658  signswmnd  31937  cardpred  32473  nummin  32474  indispconn  32594  cnllysconn  32605  ioosconn  32607  rellysconn  32611  fmlaomn0  32750  gonan0  32752  goaln0  32753  soseq  33209  fneref  33811  dnicn  33944  f1omptsnlem  34753  isbasisrelowl  34775  poimirlem27  35084  mblfinlem1  35094  mblfinlem2  35095  exidu1  35294  rngoideu  35341  isomliN  36535  idlaut  37392  resubf  39519  sn-subf  39565  mzpclall  39668  frmx  39854  frmy  39855  kelac2lem  40008  ontric3g  40230  clsk1indlem3  40746  icof  41848  sprsymrelf1  44013  fmtnof1  44052  prmdvdsfmtnof1  44104  uspgrsprf1  44375  plusfreseq  44392  nnsgrpmgm  44436  nnsgrp  44437  nn0mnd  44439  2zrngamgm  44563  2zrngmmgm  44570  2zrngnmrid  44574  ldepslinc  44918  rrx2xpref1o  45132  rrx2plordisom  45137