Theorem rgen2 3177

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052

This theorem is referenced by:  rgen3  3182  invdisjrab  5072  sosn  5718  isoid  7284  f1owe  7308  epweon  7729  epweonALT  7730  f1stres  7966  f2ndres  7967  fnwelem  8081  soseq  8109  issmo  8288  oawordeulem  8489  naddf  8617  ecopover  8768  unfilem2  9216  dffi2  9336  inficl  9338  fipwuni  9339  fisn  9340  dffi3  9344  cantnfvalf  9586  r111  9699  alephf1  10007  alephiso  10020  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem9  10081  ackbij1lem17  10157  fin1a2lem2  10323  fin1a2lem4  10325  axcc2lem  10358  smobeth  10509  nqereu  10852  addpqf  10867  mulpqf  10869  genpdm  10925  axaddf  11068  axmulf  11069  subf  11395  mulnzcnf  11796  negiso  12136  cnref1o  12935  xaddf  13176  xmulf  13224  ioof  13400  om2uzf1oi  13915  om2uzisoi  13916  wrd2ind  14685  wwlktovf1  14919  reeff1  16087  divalglem9  16370  bitsf1  16415  smupf  16447  gcdf  16481  eucalgf  16552  qredeu  16627  1arith  16898  vdwapf  16943  xpsff1o  17531  catideu  17641  sscres  17790  fpwipodrs  18506  letsr  18559  chninf  18601  mgmidmo  18628  frmdplusg  18822  efmndmgm  18853  smndex1mgm  18878  pwmnd  18908  mulgfval  19045  nmznsg  19143  efgmf  19688  efglem  19691  efgred  19723  isabli  19771  brric  20481  xrsmgm  21387  xrsds  21390  cnsubmlem  21395  cnsubrglem  21397  nn0srg  21417  rge0srg  21418  xrs1cmn  21422  xrge0subm  21423  xrge0omnd  21425  pzriprnglem5  21465  pzriprnglem8  21468  rzgrp  21603  fibas  22942  fctop  22969  cctop  22971  iccordt  23179  txuni2  23530  fsubbas  23832  zfbas  23861  ismeti  24290  dscmet  24537  qtopbaslem  24723  tgqioo  24765  xrsxmet  24775  xrsdsre  24776  retopconn  24795  iccconn  24796  divcn  24835  abscncf  24868  recncf  24869  imcncf  24870  cjcncf  24871  iimulcn  24905  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  cnllycmp  24923  bndth  24925  iundisj2  25516  dyadf  25558  reefiso  26413  recosf1o  26499  cxpcn3  26712  sgmf  27108  2lgslem1b  27355  lrcut  27896  addsf  27974  negcut  28031  negsf1o  28046  subsf  28056  mulcutlem  28123  oniso  28263  bdayn0sf1o  28362  zsoring  28401  tgjustf  28541  ercgrg  28585  2wspmdisj  30407  isabloi  30622  smcnlem  30768  cncph  30890  hvsubf  31086  hhip  31248  hhph  31249  helch  31314  hsn0elch  31319  hhssabloilem  31332  hhshsslem2  31339  shscli  31388  shintcli  31400  pjmf1  31787  idunop  32049  0cnop  32050  0cnfn  32051  idcnop  32052  idhmop  32053  0hmop  32054  adj0  32065  lnophsi  32072  lnopunii  32083  lnophmi  32089  nlelshi  32131  riesz4i  32134  cnlnadjlem6  32143  cnlnadjlem9  32146  adjcoi  32171  bra11  32179  pjhmopi  32217  iundisj2f  32660  iundisj2fi  32870  xrstos  33070  reofld  33403  xrge0slmod  33408  zringfrac  33614  iistmd  34046  cnre2csqima  34055  mndpluscn  34070  raddcn  34073  xrge0iifiso  34079  xrge0iifmhm  34083  xrge0pluscn  34084  cnzh  34112  rezh  34113  br2base  34413  sxbrsiga  34434  signswmnd  34701  cardpred  35235  nummin  35236  indispconn  35416  cnllysconn  35427  ioosconn  35429  rellysconn  35433  fmlaomn0  35572  gonan0  35574  goaln0  35575  mpomulnzcnf  36481  fneref  36532  dnicn  36752  f1omptsnlem  37652  isbasisrelowl  37674  poimirlem27  37968  mblfinlem1  37978  mblfinlem2  37979  exidu1  38177  rngoideu  38224  isomliN  39685  idlaut  40542  resubf  42813  sn-subf  42861  mzpclall  43159  frmx  43341  frmy  43342  kelac2lem  43492  onsucf1o  43700  ontric3g  43949  clsk1indlem3  44470  wfaxpr  45425  icof  45648  natglobalincr  47307  sprsymrelf1  47956  fmtnof1  47998  prmdvdsfmtnof1  48050  usgrexmpl2trifr  48513  uspgrsprf1  48623  plusfreseq  48640  nnsgrpmgm  48652  nnsgrp  48653  nn0mnd  48655  2zrngamgm  48721  2zrngmmgm  48728  2zrngnmrid  48732  ldepslinc  48985  rrx2xpref1o  49194  rrx2plordisom  49199  rescofuf  49568  oppff1  49623