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  5738  isoid  7339  f1owe  7363  f1oweOLD  7364  epweon  7791  epweonALT  7792  f1stres  8027  f2ndres  8028  fnwelem  8147  soseq  8180  issmo  8361  oawordeulem  8567  naddf  8696  ecopover  8847  unfilem2  9303  dffi2  9420  inficl  9422  fipwuni  9423  fisn  9424  dffi3  9428  cantnfvalf  9671  r111  9787  alephf1  10169  alephiso  10182  dfac5lem4  10210  kmlem9  10242  ackbij1lem17  10318  fin1a2lem2  10484  fin1a2lem4  10486  axcc2lem  10519  smobeth  10676  nqereu  11019  addpqf  11034  mulpqf  11036  genpdm  11092  axaddf  11235  axmulf  11236  subf  11564  mulnzcnf  11967  negiso  12302  cnref1o  13118  xaddf  13359  xmulf  13407  ioof  13583  om2uzf1oi  14101  om2uzisoi  14102  wrd2ind  14878  wwlktovf1  15117  reeff1  16295  divalglem9  16578  bitsf1  16623  smupf  16655  gcdf  16691  eucalgf  16765  qredeu  16840  1arith  17112  vdwapf  17157  xpsff1o  17746  catideu  17856  sscres  18005  fpwipodrs  18721  letsr  18774  chninf  18816  mgmidmo  18845  frmdplusg  19057  efmndmgm  19088  smndex1mgm  19113  pwmnd  19150  mulgfval  19286  nmznsg  19385  efgmf  19934  efglem  19937  efgred  19969  isabli  20017  xrsmgm  21720  xrsds  21723  cnsubmlem  21728  cnsubrglem  21730  nn0srg  21750  rge0srg  21751  xrs1cmn  21755  xrge0subm  21756  xrge0omnd  21758  pzriprnglem5  21798  pzriprnglem8  21801  rzgrp  21936  fibas  23302  fctop  23329  cctop  23331  iccordt  23539  txuni2  23891  fsubbas  24193  zfbas  24222  ismeti  24651  dscmet  24898  qtopbaslem  25084  tgqioo  25126  xrsxmet  25136  xrsdsre  25137  retopconn  25156  iccconn  25157  divcn  25196  abscncf  25229  recncf  25230  imcncf  25231  cjcncf  25232  iimulcn  25266  icopnfhmeo  25271  iccpnfhmeo  25273  xrhmeo  25274  cnllycmp  25284  bndth  25286  iundisj2  25877  dyadf  25919  reefiso  26782  recosf1o  26870  cxpcn3  27083  sgmf  27479  2lgslem1b  27726  lrcut  28297  addsf  28375  negcut  28432  negsf1o  28447  subsf  28457  mulcutlem  28524  oniso  28664  bdayn0sf1o  28763  zsoring  28802  tgjustf  28942  ercgrg  28987  2wspmdisj  30945  isabloi  31160  smcnlem  31306  cncph  31428  hvsubf  31624  hhip  31786  hhph  31787  helch  31852  hsn0elch  31857  hhssabloilem  31870  hhshsslem2  31877  shscli  31926  shintcli  31938  pjmf1  32325  idunop  32587  0cnop  32588  0cnfn  32589  idcnop  32590  idhmop  32591  0hmop  32592  adj0  32603  lnophsi  32610  lnopunii  32621  lnophmi  32627  nlelshi  32669  riesz4i  32672  cnlnadjlem6  32681  cnlnadjlem9  32684  adjcoi  32709  bra11  32717  pjhmopi  32755  iundisj2f  33233  iundisj2fi  33437  xrstos  33619  reofld  33952  xrge0slmod  33957  zringfrac  34134  iistmd  34582  cnre2csqima  34591  mndpluscn  34606  raddcn  34609  xrge0iifiso  34615  xrge0iifmhm  34619  xrge0pluscn  34620  cnzh  34648  rezh  34649  br2base  34949  sxbrsiga  34970  signswmnd  35234  cardpred  35775  nummin  35776  indispconn  36087  cnllysconn  36098  ioosconn  36100  rellysconn  36104  fmlaomn0  36243  gonan0  36245  goaln0  36246  mpomulnzcnf  37182  fneref  37232  dnicn  37452  f1omptsnlem  38366  isbasisrelowl  38388  poimirlem27  38672  mblfinlem1  38682  mblfinlem2  38683  exidu1  38897  rngoideu  38944  isomliN  40403  idlaut  41260  resubf  43539  sn-subf  43587  mzpclall  43845  frmx  44027  frmy  44028  kelac2lem  44173  onsucf1o  44381  ontric3g  44630  clsk1indlem3  45150  wfaxpr  46095  hashomiso  46122  icof  46339  sprsymrelf1  48685  fmtnof1  48727  prmdvdsfmtnof1  48779  usgrexmpl2trifr  49242  uspgrsprf1  49352  plusfreseq  49368  nnsgrpmgm  49380  nnsgrp  49381  nn0mnd  49383  2zrngamgm  49449  2zrngmmgm  49456  2zrngnmrid  49460  ldepslinc  49728  rrx2plordisom  49943  rescofuf  50315  oppff1  50371