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

Theorem 19.37v 1842
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 1606 . 2  |-  F/ x ph
2119.37 1811 1  |-  ( E. x ( ph  ->  ps )  <->  ( ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   E.wex 1529
This theorem is referenced by:  19.37aiv  1843  moanim  2201  axrep5  4138  kmlem14  7785  kmlem15  7786  19.37vv  26983  pm11.61  26992  rmoanim  27337  relopabVD  27946  bnj132  28020  bnj1098  28083  bnj150  28176  bnj865  28223  bnj996  28255  bnj1021  28264  bnj1090  28277  bnj1176  28303
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
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533
  Copyright terms: Public domain W3C validator