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

Theorem 19.43 1592
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 1569 . . 3  |-  ( E. x ( ph  \/  ps )  <->  E. x ( -. 
ph  ->  ps ) )
3 19.35 1587 . . 3  |-  ( E. x ( -.  ph  ->  ps )  <->  ( A. x  -.  ph  ->  E. x ps ) )
4 alnex 1530 . . . 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 1527   E.wex 1528
This theorem is referenced by:  19.34  1675  19.44  1815  19.45  1816  rexun  3356  unipr  3842  uniun  3847  unopab  4096  zfpair  4211  dmun  4884  coundi  5172  coundir  5173  kmlem16  7787  vdwapun  13017  pm10.42  26970
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator