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

Theorem 19.37v 2032
Description: Special case of Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.37v  |-  ( E. x ( ph  ->  ps )  <->  ( ph  ->  E. x ps ) )
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem 19.37v
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ph
2119.37 1790 1  |-  ( E. x ( ph  ->  ps )  <->  ( ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   E.wex 1537
This theorem is referenced by:  19.37aiv  2033  moanim  2169  axrep5  4033  kmlem14  7673  kmlem15  7674  19.37vv  26749  pm11.61  26758  relopabVD  27464  bnj132  27538  bnj1098  27601  bnj150  27694  bnj865  27741  bnj996  27773  bnj1021  27782  bnj1090  27795  bnj1176  27821
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator