Theorem rgen2 3202

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  rgen3  3207  invdisjrab  5089  sosn  5737  isoid  7337  f1owe  7361  f1oweOLD  7362  epweon  7789  epweonALT  7790  f1stres  8025  f2ndres  8026  fnwelem  8143  soseq  8176  issmo  8356  oawordeulem  8562  naddf  8691  ecopover  8842  unfilem2  9298  dffi2  9415  inficl  9417  fipwuni  9418  fisn  9419  dffi3  9423  cantnfvalf  9666  r111  9782  alephf1  10164  alephiso  10177  dfac5lem4  10205  kmlem9  10237  ackbij1lem17  10313  fin1a2lem2  10479  fin1a2lem4  10481  axcc2lem  10514  smobeth  10671  nqereu  11014  addpqf  11029  mulpqf  11031  genpdm  11087  axaddf  11230  axmulf  11231  subf  11559  mulnzcnf  11962  negiso  12297  cnref1o  13113  xaddf  13354  xmulf  13402  ioof  13578  om2uzf1oi  14096  om2uzisoi  14097  wrd2ind  14872  wwlktovf1  15110  reeff1  16288  divalglem9  16571  bitsf1  16616  smupf  16648  gcdf  16684  eucalgf  16758  qredeu  16833  1arith  17105  vdwapf  17150  xpsff1o  17739  catideu  17849  sscres  17998  fpwipodrs  18714  letsr  18767  chninf  18809  mgmidmo  18838  frmdplusg  19050  efmndmgm  19081  smndex1mgm  19106  pwmnd  19143  mulgfval  19279  nmznsg  19378  efgmf  19927  efglem  19930  efgred  19962  isabli  20010  brric  20745  xrsmgm  21713  xrsds  21716  cnsubmlem  21721  cnsubrglem  21723  nn0srg  21743  rge0srg  21744  xrs1cmn  21748  xrge0subm  21749  xrge0omnd  21751  pzriprnglem5  21791  pzriprnglem8  21794  rzgrp  21929  fibas  23295  fctop  23322  cctop  23324  iccordt  23532  txuni2  23884  fsubbas  24186  zfbas  24215  ismeti  24644  dscmet  24891  qtopbaslem  25077  tgqioo  25119  xrsxmet  25129  xrsdsre  25130  retopconn  25149  iccconn  25150  divcn  25189  abscncf  25222  recncf  25223  imcncf  25224  cjcncf  25225  iimulcn  25259  icopnfhmeo  25264  iccpnfhmeo  25266  xrhmeo  25267  cnllycmp  25277  bndth  25279  iundisj2  25870  dyadf  25912  reefiso  26775  recosf1o  26863  cxpcn3  27076  sgmf  27472  2lgslem1b  27719  lrcut  28290  addsf  28368  negcut  28425  negsf1o  28440  subsf  28450  mulcutlem  28517  oniso  28657  bdayn0sf1o  28756  zsoring  28795  tgjustf  28935  ercgrg  28980  2wspmdisj  30938  isabloi  31153  smcnlem  31299  cncph  31421  hvsubf  31617  hhip  31779  hhph  31780  helch  31845  hsn0elch  31850  hhssabloilem  31863  hhshsslem2  31870  shscli  31919  shintcli  31931  pjmf1  32318  idunop  32580  0cnop  32581  0cnfn  32582  idcnop  32583  idhmop  32584  0hmop  32585  adj0  32596  lnophsi  32603  lnopunii  32614  lnophmi  32620  nlelshi  32662  riesz4i  32665  cnlnadjlem6  32674  cnlnadjlem9  32677  adjcoi  32702  bra11  32710  pjhmopi  32748  iundisj2f  33184  iundisj2fi  33389  xrstos  33571  reofld  33904  xrge0slmod  33909  zringfrac  34086  iistmd  34534  cnre2csqima  34543  mndpluscn  34558  raddcn  34561  xrge0iifiso  34567  xrge0iifmhm  34571  xrge0pluscn  34572  cnzh  34600  rezh  34601  br2base  34901  sxbrsiga  34922  signswmnd  35186  cardpred  35721  nummin  35722  indispconn  35999  cnllysconn  36010  ioosconn  36012  rellysconn  36016  fmlaomn0  36155  gonan0  36157  goaln0  36158  mpomulnzcnf  37088  fneref  37138  dnicn  37358  f1omptsnlem  38260  isbasisrelowl  38282  poimirlem27  38566  mblfinlem1  38576  mblfinlem2  38577  exidu1  38791  rngoideu  38838  isomliN  40297  idlaut  41154  resubf  43433  sn-subf  43481  mzpclall  43738  frmx  43920  frmy  43921  kelac2lem  44066  onsucf1o  44274  ontric3g  44523  clsk1indlem3  45043  wfaxpr  45988  hashomiso  46015  icof  46232  sprsymrelf1  48578  fmtnof1  48620  prmdvdsfmtnof1  48672  usgrexmpl2trifr  49135  uspgrsprf1  49245  plusfreseq  49261  nnsgrpmgm  49273  nnsgrp  49274  nn0mnd  49276  2zrngamgm  49342  2zrngmmgm  49349  2zrngnmrid  49353  ldepslinc  49621  rrx2xpref1o  49830  rrx2plordisom  49835  rescofuf  50201  oppff1  50256