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

Theorem 19.21bi 1774
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
19.21bi.1  |-  ( ph  ->  A. x ps )
Assertion
Ref Expression
19.21bi  |-  ( ph  ->  ps )

Proof of Theorem 19.21bi
StepHypRef Expression
1 19.21bi.1 . 2  |-  ( ph  ->  A. x ps )
2 ax-4 1692 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 17 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532
This theorem is referenced by:  19.21bbi  1775  eqeq1  2259  eleq2  2314  r19.21bi  2603  ssel  3097  copsex2t  4146  pocl  4214  funmo  5129  funun  5153  fununi  5173  findcard  6982  findcard2  6983  axpowndlem2  8100  axpowndlem4  8102  axregndlem2  8105  axinfnd  8108  prcdnq  8497  relexpindlem  23207  dfrtrcl2  23216  imfstnrelc  24246  cmpmon  24981  vk15.4j  27081  hbimpg  27110  bnj1379  27649  bnj1052  27791  bnj1118  27800  bnj1154  27815  bnj1280  27836
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10  ax-4 1692
  Copyright terms: Public domain W3C validator