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

Theorem 19.43 1594
Description: Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
Assertion
Ref Expression
19.43  |-  ( E. x ( ph  \/  ps )  <->  ( E. x ph  \/  E. x ps ) )

Proof of Theorem 19.43
StepHypRef Expression
1 df-or 359 . . . 4  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
21exbii 1571 . . 3  |-  ( E. x ( ph  \/  ps )  <->  E. x ( -. 
ph  ->  ps ) )
3 19.35 1589 . . 3  |-  ( E. x ( -.  ph  ->  ps )  <->  ( A. x  -.  ph  ->  E. x ps ) )
4 alnex 1532 . . . 4  |-  ( A. x  -.  ph  <->  -.  E. x ph )
54imbi1i 315 . . 3  |-  ( ( A. x  -.  ph  ->  E. x ps )  <->  ( -.  E. x ph  ->  E. x ps )
)
62, 3, 53bitri 262 . 2  |-  ( E. x ( ph  \/  ps )  <->  ( -.  E. x ph  ->  E. x ps ) )
7 df-or 359 . 2  |-  ( ( E. x ph  \/  E. x ps )  <->  ( -.  E. x ph  ->  E. x ps ) )
86, 7bitr4i 243 1  |-  ( E. x ( ph  \/  ps )  <->  ( E. x ph  \/  E. x ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357   A.wal 1529   E.wex 1530
This theorem is referenced by:  19.34  1676  19.44  1815  19.45  1816  rexun  3357  unipr  3843  uniun  3848  unopab  4097  zfpair  4214  dmun  4887  coundi  5176  coundir  5177  kmlem16  7793  vdwapun  13023  pm10.42  27570
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-ex 1531
  Copyright terms: Public domain W3C validator