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

Theorem 19.37v 1769
Description: Version of 19.37 1967 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-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 19.35 1688 . 2  |-  ( E. x ( ph  ->  ps )  <->  ( A. x ph  ->  E. x ps )
)
2 19.3v 1756 . . 3  |-  ( A. x ph  <->  ph )
32imbi1i 325 . 2  |-  ( ( A. x ph  ->  E. x ps )  <->  ( ph  ->  E. x ps )
)
41, 3bitri 249 1  |-  ( E. x ( ph  ->  ps )  <->  ( ph  ->  E. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1393   E.wex 1613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748
This theorem depends on definitions:  df-bi 185  df-ex 1614
This theorem is referenced by:  19.37iv  1770  axrep5  4573  fvn0ssdmfun  6023  kmlem14  8560  kmlem15  8561  eqvincg  27501  19.37vv  31494  pm11.61  31503  rmoanim  32387  relopabVD  33844  bnj132  33922  bnj1098  33985  bnj150  34077  bnj865  34124  bnj996  34156  bnj1021  34165  bnj1090  34178  bnj1176  34204  bj-axrep5  34521
  Copyright terms: Public domain W3C validator