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

Theorem 19.21bi 1806
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 1728 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 15 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530
This theorem is referenced by:  19.21bbi  1807  eqeq1  2302  eleq2  2357  r19.21bi  2654  ssel  3187  copsex2t  4269  pocl  4337  funmo  5287  funun  5312  fununi  5332  findcard  7113  findcard2  7114  axpowndlem2  8236  axpowndlem4  8238  axregndlem2  8241  axinfnd  8244  prcdnq  8633  relexpindlem  24051  dfrtrcl2  24060  imfstnrelc  25184  cmpmon  25918  vk15.4j  28590  hbimpg  28619  bnj1379  29179  bnj1052  29321  bnj1118  29330  bnj1154  29345  bnj1280  29366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
  Copyright terms: Public domain W3C validator