Theorem rgen2 3207

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3082

This theorem is used by:  rgen3  3212  invdisjrab  5098  sosn  5750  isoid  7333  f1owe  7357  f1oweOLD  7358  epweon  7776  epweonALT  7777  f1stres  8012  f2ndres  8013  fnwelem  8129  soseq  8157  issmo  8337  oawordeulem  8541  naddf  8670  ecopover  8821  unfilem2  9269  dffi2  9386  inficl  9388  fipwuni  9389  fisn  9390  dffi3  9394  cantnfvalf  9637  r111  9750  alephf1  10081  alephiso  10094  dfac5lem4  10122  kmlem9  10154  ackbij1lem17  10230  fin1a2lem2  10396  fin1a2lem4  10398  axcc2lem  10431  smobeth  10582  nqereu  10925  addpqf  10940  mulpqf  10942  genpdm  10998  axaddf  11141  axmulf  11142  subf  11470  mulnzcnf  11871  negiso  12206  cnref1o  13021  xaddf  13262  xmulf  13310  ioof  13486  om2uzf1oi  14003  om2uzisoi  14004  wrd2ind  14778  wwlktovf1  15014  reeff1  16194  divalglem9  16477  bitsf1  16522  smupf  16554  gcdf  16588  eucalgf  16659  qredeu  16734  1arith  17005  vdwapf  17050  xpsff1o  17639  catideu  17749  sscres  17898  fpwipodrs  18614  letsr  18667  chninf  18709  mgmidmo  18736  frmdplusg  18937  efmndmgm  18968  smndex1mgm  18993  pwmnd  19023  mulgfval  19159  nmznsg  19258  efgmf  19807  efglem  19810  efgred  19842  isabli  19890  brric  20623  xrsmgm  21587  xrsds  21590  cnsubmlem  21595  cnsubrglem  21597  nn0srg  21617  rge0srg  21618  xrs1cmn  21622  xrge0subm  21623  xrge0omnd  21625  pzriprnglem5  21665  pzriprnglem8  21668  rzgrp  21803  fibas  23164  fctop  23191  cctop  23193  iccordt  23401  txuni2  23753  fsubbas  24055  zfbas  24084  ismeti  24513  dscmet  24760  qtopbaslem  24946  tgqioo  24988  xrsxmet  24998  xrsdsre  24999  retopconn  25018  iccconn  25019  divcn  25058  abscncf  25091  recncf  25092  imcncf  25093  cjcncf  25094  iimulcn  25128  icopnfhmeo  25133  iccpnfhmeo  25135  xrhmeo  25136  cnllycmp  25146  bndth  25148  iundisj2  25739  dyadf  25781  reefiso  26642  recosf1o  26731  cxpcn3  26944  sgmf  27340  2lgslem1b  27587  lrcut  28128  addsf  28206  negcut  28263  negsf1o  28278  subsf  28288  mulcutlem  28355  oniso  28495  bdayn0sf1o  28594  zsoring  28633  tgjustf  28773  ercgrg  28817  2wspmdisj  30735  isabloi  30950  smcnlem  31096  cncph  31218  hvsubf  31414  hhip  31576  hhph  31577  helch  31642  hsn0elch  31647  hhssabloilem  31660  hhshsslem2  31667  shscli  31716  shintcli  31728  pjmf1  32115  idunop  32377  0cnop  32378  0cnfn  32379  idcnop  32380  idhmop  32381  0hmop  32382  adj0  32393  lnophsi  32400  lnopunii  32411  lnophmi  32417  nlelshi  32459  riesz4i  32462  cnlnadjlem6  32471  cnlnadjlem9  32474  adjcoi  32499  bra11  32507  pjhmopi  32545  iundisj2f  32982  iundisj2fi  33188  xrstos  33370  reofld  33703  xrge0slmod  33708  zringfrac  33884  iistmd  34332  cnre2csqima  34341  mndpluscn  34356  raddcn  34359  xrge0iifiso  34365  xrge0iifmhm  34369  xrge0pluscn  34370  cnzh  34398  rezh  34399  br2base  34700  sxbrsiga  34721  signswmnd  34985  cardpred  35517  nummin  35518  indispconn  35739  cnllysconn  35750  ioosconn  35752  rellysconn  35756  fmlaomn0  35895  gonan0  35897  goaln0  35898  mpomulnzcnf  36844  fneref  36894  dnicn  37114  f1omptsnlem  38015  isbasisrelowl  38037  poimirlem27  38331  mblfinlem1  38341  mblfinlem2  38342  exidu1  38540  rngoideu  38587  isomliN  40046  idlaut  40903  resubf  43175  sn-subf  43223  mzpclall  43491  frmx  43673  frmy  43674  kelac2lem  43824  onsucf1o  44032  ontric3g  44281  clsk1indlem3  44802  wfaxpr  45740  hashomiso  45767  icof  45968  natglobalincr  47626  sprsymrelf1  48278  fmtnof1  48320  prmdvdsfmtnof1  48372  usgrexmpl2trifr  48835  uspgrsprf1  48945  plusfreseq  48962  nnsgrpmgm  48974  nnsgrp  48975  nn0mnd  48977  2zrngamgm  49043  2zrngmmgm  49050  2zrngnmrid  49054  ldepslinc  49322  rrx2xpref1o  49531  rrx2plordisom  49536  rescofuf  49904  oppff1  49959