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

Theorem 19.37v 1911
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 1626 . 2  |-  F/ x ph
2119.37 1883 1  |-  ( E. x ( ph  ->  ps )  <->  ( ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1547
This theorem is referenced by:  19.37aiv  1912  moanim  2287  axrep5  4259  kmlem14  7969  kmlem15  7970  eqvincg  23798  19.37vv  27245  pm11.61  27254  rmoanim  27618  relopabVD  28347  bnj132  28422  bnj1098  28485  bnj150  28578  bnj865  28625  bnj996  28657  bnj1021  28666  bnj1090  28679  bnj1176  28705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator