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

Theorem 19.21bi 1775
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 1764 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550
This theorem is referenced by:  19.21bbi  1889  equveli  2086  eqeq1  2444  eleq2  2499  r19.21bi  2806  ssel  3344  copsex2t  4446  pocl  4513  funmo  5473  funun  5498  fununi  5520  findcard  7350  findcard2  7351  axpowndlem2  8478  axpowndlem4  8480  axregndlem2  8483  axinfnd  8486  prcdnq  8875  relexpindlem  25144  dfrtrcl2  25153  vk15.4j  28686  hbimpg  28715  bnj1379  29276  bnj1052  29418  bnj1118  29427  bnj1154  29442  bnj1280  29463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator