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

Theorem 19.37v 1922
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 1894 1  |-  ( E. x ( ph  ->  ps )  <->  ( ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1550
This theorem is referenced by:  19.37aiv  1923  moanim  2336  axrep5  4317  kmlem14  8032  kmlem15  8033  eqvincg  23949  19.37vv  27498  pm11.61  27507  rmoanim  27871  relopabVD  28867  bnj132  28945  bnj1098  29008  bnj150  29101  bnj865  29148  bnj996  29180  bnj1021  29189  bnj1090  29202  bnj1176  29228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator