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

Theorem 19.21bi 1794
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 sp 1716 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 15 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527
This theorem is referenced by:  19.21bbi  1795  eqeq1  2289  eleq2  2344  r19.21bi  2641  ssel  3174  copsex2t  4253  pocl  4321  funmo  5271  funun  5296  fununi  5316  findcard  7097  findcard2  7098  axpowndlem2  8220  axpowndlem4  8222  axregndlem2  8225  axinfnd  8228  prcdnq  8617  relexpindlem  24036  dfrtrcl2  24045  imfstnrelc  25081  cmpmon  25815  vk15.4j  28291  hbimpg  28320  bnj1379  28863  bnj1052  29005  bnj1118  29014  bnj1154  29029  bnj1280  29050
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
  Copyright terms: Public domain W3C validator