Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.29r Structured version   Unicode version

Theorem r19.29r 2942
 Description: Restricted quantifier version of 19.29r 1705; variation of r19.29 2941. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
r19.29r

Proof of Theorem r19.29r
StepHypRef Expression
1 r19.29 2941 . 2
2 ancom 448 . 2
3 ancom 448 . . 3
43rexbii 2905 . 2
51, 2, 43imtr4i 266 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 367  wral 2753  wrex 2754 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652 This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-ral 2758  df-rex 2759 This theorem is referenced by:  r19.29imd  2943  r19.29af2OLD  2945  2reu5  3257  rlimuni  13429  rlimno1  13532  neindisj2  19809  lmss  19984  fclsbas  20706  isfcf  20719  ucnima  20968  metcnp3  21227  cfilucfilOLD  21256  cfilucfil  21257  bndth  21642  ellimc3  22467  lmxrge0  28267  gsumesum  28386  esumcst  28390  esumfsup  28397  voliune  28558  volfiniune  28559  bnj517  29151  cover2  31467  prmunb2  36020
 Copyright terms: Public domain W3C validator