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

Theorem 19.37v 1923
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 1630 . 2  |-  F/ x ph
2119.37 1895 1  |-  ( E. x ( ph  ->  ps )  <->  ( ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   E.wex 1551
This theorem is referenced by:  19.37aiv  1924  moanim  2339  axrep5  4328  kmlem14  8048  kmlem15  8049  eqvincg  23966  19.37vv  27574  pm11.61  27583  rmoanim  27947  relopabVD  29087  bnj132  29165  bnj1098  29228  bnj150  29321  bnj865  29368  bnj996  29400  bnj1021  29409  bnj1090  29422  bnj1176  29448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator