Theorem rgen2 3201

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3076

This theorem is referenced by:  rgen3  3206  invdisjrab  5084  sosn  5730  isoid  7308  f1owe  7332  epweon  7753  epweonALT  7754  f1stres  7989  f2ndres  7990  fnwelem  8105  soseq  8133  issmo  8313  oawordeulem  8517  naddf  8646  ecopover  8797  unfilem2  9244  dffi2  9363  inficl  9365  fipwuni  9366  fisn  9367  dffi3  9371  cantnfvalf  9614  r111  9727  alephf1  10035  alephiso  10048  dfac5lem4  10076  dfac5lem4OLD  10078  kmlem9  10109  ackbij1lem17  10185  fin1a2lem2  10352  fin1a2lem4  10354  axcc2lem  10387  smobeth  10538  nqereu  10881  addpqf  10896  mulpqf  10898  genpdm  10954  axaddf  11097  axmulf  11098  subf  11426  mulnzcnf  11827  negiso  12166  cnref1o  12980  xaddf  13221  xmulf  13269  ioof  13445  om2uzf1oi  13960  om2uzisoi  13961  wrd2ind  14730  wwlktovf1  14964  reeff1  16143  divalglem9  16426  bitsf1  16471  smupf  16503  gcdf  16537  eucalgf  16608  qredeu  16683  1arith  16954  vdwapf  16999  xpsff1o  17588  catideu  17698  sscres  17847  fpwipodrs  18563  letsr  18616  chninf  18658  mgmidmo  18685  frmdplusg  18879  efmndmgm  18910  smndex1mgm  18935  pwmnd  18965  mulgfval  19102  nmznsg  19200  efgmf  19744  efglem  19747  efgred  19779  isabli  19827  brric  20540  xrsmgm  21447  xrsds  21450  cnsubmlem  21455  cnsubrglem  21457  nn0srg  21477  rge0srg  21478  xrs1cmn  21482  xrge0subm  21483  xrge0omnd  21485  pzriprnglem5  21525  pzriprnglem8  21528  rzgrp  21663  fibas  23025  fctop  23052  cctop  23054  iccordt  23262  txuni2  23613  fsubbas  23915  zfbas  23944  ismeti  24373  dscmet  24620  qtopbaslem  24806  tgqioo  24848  xrsxmet  24858  xrsdsre  24859  retopconn  24878  iccconn  24879  divcn  24918  abscncf  24951  recncf  24952  imcncf  24953  cjcncf  24954  iimulcn  24988  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  cnllycmp  25006  bndth  25008  iundisj2  25599  dyadf  25641  reefiso  26499  recosf1o  26588  cxpcn3  26801  sgmf  27197  2lgslem1b  27444  lrcut  27985  addsf  28063  negcut  28120  negsf1o  28135  subsf  28145  mulcutlem  28212  oniso  28352  bdayn0sf1o  28451  zsoring  28490  tgjustf  28630  ercgrg  28674  2wspmdisj  30496  isabloi  30711  smcnlem  30857  cncph  30979  hvsubf  31175  hhip  31337  hhph  31338  helch  31403  hsn0elch  31408  hhssabloilem  31421  hhshsslem2  31428  shscli  31477  shintcli  31489  pjmf1  31876  idunop  32138  0cnop  32139  0cnfn  32140  idcnop  32141  idhmop  32142  0hmop  32143  adj0  32154  lnophsi  32161  lnopunii  32172  lnophmi  32178  nlelshi  32220  riesz4i  32223  cnlnadjlem6  32232  cnlnadjlem9  32235  adjcoi  32260  bra11  32268  pjhmopi  32306  iundisj2f  32750  iundisj2fi  32960  xrstos  33149  reofld  33490  xrge0slmod  33495  zringfrac  33711  iistmd  34160  cnre2csqima  34169  mndpluscn  34184  raddcn  34187  xrge0iifiso  34193  xrge0iifmhm  34197  xrge0pluscn  34198  cnzh  34226  rezh  34227  br2base  34527  sxbrsiga  34548  signswmnd  34812  cardpred  35349  nummin  35350  indispconn  35545  cnllysconn  35556  ioosconn  35558  rellysconn  35562  fmlaomn0  35701  gonan0  35703  goaln0  35704  mpomulnzcnf  36620  fneref  36671  dnicn  36891  f1omptsnlem  37791  isbasisrelowl  37813  poimirlem27  38107  mblfinlem1  38117  mblfinlem2  38118  exidu1  38316  rngoideu  38363  isomliN  39824  idlaut  40681  resubf  42951  sn-subf  42999  mzpclall  43269  frmx  43451  frmy  43452  kelac2lem  43602  onsucf1o  43810  ontric3g  44059  clsk1indlem3  44580  wfaxpr  45535  icof  45756  natglobalincr  47414  sprsymrelf1  48063  fmtnof1  48105  prmdvdsfmtnof1  48157  usgrexmpl2trifr  48620  uspgrsprf1  48730  plusfreseq  48747  nnsgrpmgm  48759  nnsgrp  48760  nn0mnd  48762  2zrngamgm  48828  2zrngmmgm  48835  2zrngnmrid  48839  ldepslinc  49092  rrx2xpref1o  49301  rrx2plordisom  49306  rescofuf  49675  oppff1  49730