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

Theorem 19.37v 1840
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 1605 . 2  |-  F/ x ph
2119.37 1809 1  |-  ( E. x ( ph  ->  ps )  <->  ( ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1528
This theorem is referenced by:  19.37aiv  1841  moanim  2199  axrep5  4136  kmlem14  7789  kmlem15  7790  eqvincg  23130  19.37vv  27583  pm11.61  27592  rmoanim  27957  relopabVD  28677  bnj132  28752  bnj1098  28815  bnj150  28908  bnj865  28955  bnj996  28987  bnj1021  28996  bnj1090  29009  bnj1176  29035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator