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

Theorem 19.43 1610
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 1587 . . 3  |-  ( E. x ( ph  \/  ps )  <->  E. x ( -. 
ph  ->  ps ) )
3 19.35 1605 . . 3  |-  ( E. x ( -.  ph  ->  ps )  <->  ( A. x  -.  ph  ->  E. x ps ) )
4 alnex 1548 . . . 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 1545   E.wex 1546
This theorem is referenced by:  19.34  1668  19.44  1885  19.45  1886  rexun  3443  unipr  3943  uniun  3948  unopab  4197  zfpair  4314  dmun  4988  coundi  5277  coundir  5278  kmlem16  7938  vdwapun  13229  usgraedg4  21083  pm10.42  27065
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-ex 1547
  Copyright terms: Public domain W3C validator