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

Theorem 19.21bi 1796
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 1717 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 17 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1528
This theorem is referenced by:  19.21bbi  1797  eqeq1  2291  eleq2  2346  r19.21bi  2643  ssel  3176  copsex2t  4253  pocl  4321  funmo  5238  funun  5262  fununi  5282  findcard  7093  findcard2  7094  axpowndlem2  8216  axpowndlem4  8218  axregndlem2  8221  axinfnd  8224  prcdnq  8613  relexpindlem  23441  dfrtrcl2  23450  imfstnrelc  24480  cmpmon  25215  vk15.4j  27563  hbimpg  27592  bnj1379  28131  bnj1052  28273  bnj1118  28282  bnj1154  28297  bnj1280  28318
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-11 1716
  Copyright terms: Public domain W3C validator