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 2145  ∀wral 3076

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 3077

This theorem is used by:  rgen3  3207  invdisjrab  5090  sosn  5742  isoid  7330  f1owe  7354  f1oweOLD  7355  epweon  7774  epweonALT  7775  f1stres  8010  f2ndres  8011  fnwelem  8129  soseq  8157  issmo  8337  oawordeulem  8541  naddf  8670  ecopover  8821  unfilem2  9276  dffi2  9393  inficl  9395  fipwuni  9396  fisn  9397  dffi3  9401  cantnfvalf  9644  r111  9757  alephf1  10088  alephiso  10101  dfac5lem4  10129  kmlem9  10161  ackbij1lem17  10237  fin1a2lem2  10403  fin1a2lem4  10405  axcc2lem  10438  smobeth  10595  nqereu  10938  addpqf  10953  mulpqf  10955  genpdm  11011  axaddf  11154  axmulf  11155  subf  11483  mulnzcnf  11884  negiso  12219  cnref1o  13035  xaddf  13276  xmulf  13324  ioof  13500  om2uzf1oi  14017  om2uzisoi  14018  wrd2ind  14792  wwlktovf1  15030  reeff1  16208  divalglem9  16491  bitsf1  16536  smupf  16568  gcdf  16602  eucalgf  16673  qredeu  16748  1arith  17019  vdwapf  17064  xpsff1o  17653  catideu  17763  sscres  17912  fpwipodrs  18628  letsr  18681  chninf  18723  mgmidmo  18752  frmdplusg  18963  efmndmgm  18994  smndex1mgm  19019  pwmnd  19056  mulgfval  19192  nmznsg  19291  efgmf  19840  efglem  19843  efgred  19875  isabli  19923  brric  20656  xrsmgm  21620  xrsds  21623  cnsubmlem  21628  cnsubrglem  21630  nn0srg  21650  rge0srg  21651  xrs1cmn  21655  xrge0subm  21656  xrge0omnd  21658  pzriprnglem5  21698  pzriprnglem8  21701  rzgrp  21836  fibas  23202  fctop  23229  cctop  23231  iccordt  23439  txuni2  23791  fsubbas  24093  zfbas  24122  ismeti  24551  dscmet  24798  qtopbaslem  24984  tgqioo  25026  xrsxmet  25036  xrsdsre  25037  retopconn  25056  iccconn  25057  divcn  25096  abscncf  25129  recncf  25130  imcncf  25131  cjcncf  25132  iimulcn  25166  icopnfhmeo  25171  iccpnfhmeo  25173  xrhmeo  25174  cnllycmp  25184  bndth  25186  iundisj2  25777  dyadf  25819  reefiso  26684  recosf1o  26772  cxpcn3  26985  sgmf  27381  2lgslem1b  27628  lrcut  28169  addsf  28247  negcut  28304  negsf1o  28319  subsf  28329  mulcutlem  28396  oniso  28536  bdayn0sf1o  28635  zsoring  28674  tgjustf  28814  ercgrg  28859  2wspmdisj  30817  isabloi  31032  smcnlem  31178  cncph  31300  hvsubf  31496  hhip  31658  hhph  31659  helch  31724  hsn0elch  31729  hhssabloilem  31742  hhshsslem2  31749  shscli  31798  shintcli  31810  pjmf1  32197  idunop  32459  0cnop  32460  0cnfn  32461  idcnop  32462  idhmop  32463  0hmop  32464  adj0  32475  lnophsi  32482  lnopunii  32493  lnophmi  32499  nlelshi  32541  riesz4i  32544  cnlnadjlem6  32553  cnlnadjlem9  32556  adjcoi  32581  bra11  32589  pjhmopi  32627  iundisj2f  33063  iundisj2fi  33268  xrstos  33450  reofld  33783  xrge0slmod  33788  zringfrac  33964  iistmd  34412  cnre2csqima  34421  mndpluscn  34436  raddcn  34439  xrge0iifiso  34445  xrge0iifmhm  34449  xrge0pluscn  34450  cnzh  34478  rezh  34479  br2base  34780  sxbrsiga  34801  signswmnd  35065  cardpred  35597  nummin  35598  indispconn  35813  cnllysconn  35824  ioosconn  35826  rellysconn  35830  fmlaomn0  35969  gonan0  35971  goaln0  35972  mpomulnzcnf  36919  fneref  36969  dnicn  37189  f1omptsnlem  38090  isbasisrelowl  38112  poimirlem27  38396  mblfinlem1  38406  mblfinlem2  38407  exidu1  38606  rngoideu  38653  isomliN  40112  idlaut  40969  resubf  43256  sn-subf  43304  mzpclall  43572  frmx  43754  frmy  43755  kelac2lem  43905  onsucf1o  44113  ontric3g  44362  clsk1indlem3  44883  wfaxpr  45821  hashomiso  45848  icof  46049  sprsymrelf1  48396  fmtnof1  48438  prmdvdsfmtnof1  48490  usgrexmpl2trifr  48953  uspgrsprf1  49063  plusfreseq  49079  nnsgrpmgm  49091  nnsgrp  49092  nn0mnd  49094  2zrngamgm  49160  2zrngmmgm  49167  2zrngnmrid  49171  ldepslinc  49439  rrx2xpref1o  49648  rrx2plordisom  49653  rescofuf  50019  oppff1  50074