Theorem rgen2 3126

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068

This theorem is referenced by:  rgen3  3127  invdisjrabw  5055  invdisjrab  5056  sosn  5664  isoid  7180  f1owe  7204  epweon  7603  f1stres  7828  f2ndres  7829  fnwelem  7943  issmo  8150  oawordeulem  8347  ecopover  8568  unfilem2  9009  dffi2  9112  inficl  9114  fipwuni  9115  fisn  9116  dffi3  9120  cantnfvalf  9353  r111  9464  alephf1  9772  alephiso  9785  dfac5lem4  9813  kmlem9  9845  ackbij1lem17  9923  fin1a2lem2  10088  fin1a2lem4  10090  axcc2lem  10123  smobeth  10273  nqereu  10616  addpqf  10631  mulpqf  10633  genpdm  10689  axaddf  10832  axmulf  10833  subf  11153  mulnzcnopr  11551  negiso  11885  cnref1o  12654  xaddf  12887  xmulf  12935  ioof  13108  om2uzf1oi  13601  om2uzisoi  13602  wrd2ind  14364  wwlktovf1  14600  reeff1  15757  divalglem9  16038  bitsf1  16081  smupf  16113  gcdf  16147  eucalgf  16216  qredeu  16291  1arith  16556  vdwapf  16601  xpsff1o  17195  catideu  17301  sscres  17452  fpwipodrs  18173  letsr  18226  mgmidmo  18259  frmdplusg  18408  efmndmgm  18439  smndex1mgm  18461  pwmnd  18491  mulgfval  18617  nmznsg  18711  efgmf  19234  efglem  19237  efgred  19269  isabli  19316  brric  19903  xrsmgm  20545  xrs1cmn  20550  xrge0subm  20551  xrsds  20553  cnsubmlem  20558  cnsubrglem  20560  nn0srg  20580  rge0srg  20581  rzgrp  20740  fibas  22035  fctop  22062  cctop  22064  iccordt  22273  txuni2  22624  fsubbas  22926  zfbas  22955  ismeti  23386  dscmet  23634  qtopbaslem  23828  tgqioo  23869  xrsxmet  23878  xrsdsre  23879  retopconn  23898  iccconn  23899  divcn  23937  abscncf  23970  recncf  23971  imcncf  23972  cjcncf  23973  iimulcn  24007  icopnfhmeo  24012  iccpnfhmeo  24014  xrhmeo  24015  cnllycmp  24025  bndth  24027  iundisj2  24618  dyadf  24660  reefiso  25512  recosf1o  25596  cxpcn3  25806  sgmf  26199  2lgslem1b  26445  tgjustf  26738  ercgrg  26782  2wspmdisj  28602  isabloi  28814  smcnlem  28960  cncph  29082  hvsubf  29278  hhip  29440  hhph  29441  helch  29506  hsn0elch  29511  hhssabloilem  29524  hhshsslem2  29531  shscli  29580  shintcli  29592  pjmf1  29979  idunop  30241  0cnop  30242  0cnfn  30243  idcnop  30244  idhmop  30245  0hmop  30246  adj0  30257  lnophsi  30264  lnopunii  30275  lnophmi  30281  nlelshi  30323  riesz4i  30326  cnlnadjlem6  30335  cnlnadjlem9  30338  adjcoi  30363  bra11  30371  pjhmopi  30409  iundisj2f  30830  iundisj2fi  31020  xrstos  31190  xrge0omnd  31239  reofld  31446  xrge0slmod  31450  iistmd  31754  cnre2csqima  31763  mndpluscn  31778  raddcn  31781  xrge0iifiso  31787  xrge0iifmhm  31791  xrge0pluscn  31792  cnzh  31820  rezh  31821  br2base  32136  sxbrsiga  32157  signswmnd  32436  cardpred  32962  nummin  32963  indispconn  33096  cnllysconn  33107  ioosconn  33109  rellysconn  33113  fmlaomn0  33252  gonan0  33254  goaln0  33255  soseq  33730  lrcut  34010  fneref  34466  dnicn  34599  f1omptsnlem  35434  isbasisrelowl  35456  poimirlem27  35731  mblfinlem1  35741  mblfinlem2  35742  exidu1  35941  rngoideu  35988  isomliN  37180  idlaut  38037  resubf  40285  sn-subf  40331  mzpclall  40465  frmx  40651  frmy  40652  kelac2lem  40805  ontric3g  41027  clsk1indlem3  41542  icof  42648  sprsymrelf1  44836  fmtnof1  44875  prmdvdsfmtnof1  44927  uspgrsprf1  45197  plusfreseq  45214  nnsgrpmgm  45258  nnsgrp  45259  nn0mnd  45261  2zrngamgm  45385  2zrngmmgm  45392  2zrngnmrid  45396  ldepslinc  45738  rrx2xpref1o  45952  rrx2plordisom  45957