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

Theorem 19.43 1604
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 361 . . . 4  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
21exbii 1580 . . 3  |-  ( E. x ( ph  \/  ps )  <->  E. x ( -. 
ph  ->  ps ) )
3 19.35 1599 . . 3  |-  ( E. x ( -.  ph  ->  ps )  <->  ( A. x  -.  ph  ->  E. x ps ) )
4 alnex 1569 . . . 4  |-  ( A. x  -.  ph  <->  -.  E. x ph )
54imbi1i 317 . . 3  |-  ( ( A. x  -.  ph  ->  E. x ps )  <->  ( -.  E. x ph  ->  E. x ps )
)
62, 3, 53bitri 264 . 2  |-  ( E. x ( ph  \/  ps )  <->  ( -.  E. x ph  ->  E. x ps ) )
7 df-or 361 . 2  |-  ( ( E. x ph  \/  E. x ps )  <->  ( -.  E. x ph  ->  E. x ps ) )
86, 7bitr4i 245 1  |-  ( E. x ( ph  \/  ps )  <->  ( E. x ph  \/  E. x ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    \/ wo 359   A.wal 1532   E.wex 1537
This theorem is referenced by:  19.44  1796  19.45  1797  19.34  1798  rexun  3263  unipr  3741  uniun  3746  unopab  3992  zfpair  4106  dmun  4792  coundi  5080  coundir  5081  kmlem16  7675  vdwapun  12895  pm10.42  26725
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-ex 1538
  Copyright terms: Public domain W3C validator