Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rgen2 Unicode version

Theorem rgen2 2882
 Description: Generalization rule for restricted quantification, with two quantifiers. (Contributed by NM, 30-May-1999.)
Hypothesis
Ref Expression
rgen2.1
Assertion
Ref Expression
rgen2
Distinct variable groups:   ,   ,

Proof of Theorem rgen2
StepHypRef Expression
1 rgen2.1 . . 3
21ralrimiva 2871 . 2
32rgen 2817 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807 This theorem is referenced by:  rgen3  2883  f1stres  6822  f2ndres  6823  smobeth  8982  disjxwrd  12680  wrd2ind  12703  smupf  14128  xpsff1o  14965  efgmf  16731  efglem  16734  txuni2  20066  divcn  21372  abscncf  21405  recncf  21406  imcncf  21407  cjcncf  21408  cnllycmp  21456  bndth  21458  dyadf  22000  cxpcn3  23122  sgmf  23419  smcnlem  25607  helch  26161  hsn0elch  26166  hhshsslem2  26184  shscli  26235  shintcli  26247  0cnop  26898  0cnfn  26899  idcnop  26900  lnophsi  26920  nlelshi  26979  cnlnadjlem6  26991  cnzh  27951  rezh  27952  cnllyscon  28690  rellyscon  28696  mblfinlem1  30051  mblfinlem2  30052  fneref  30168  frmx  30849  frmy  30850  2zrngnmrid  32756  ldepslinc  33110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704 This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812
 Copyright terms: Public domain W3C validator