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

Theorem 19.43 1660
Description: Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-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 370 . . . 4  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
21exbii 1634 . . 3  |-  ( E. x ( ph  \/  ps )  <->  E. x ( -. 
ph  ->  ps ) )
3 19.35 1654 . . 3  |-  ( E. x ( -.  ph  ->  ps )  <->  ( A. x  -.  ph  ->  E. x ps ) )
4 alnex 1588 . . . 4  |-  ( A. x  -.  ph  <->  -.  E. x ph )
54imbi1i 325 . . 3  |-  ( ( A. x  -.  ph  ->  E. x ps )  <->  ( -.  E. x ph  ->  E. x ps )
)
62, 3, 53bitri 271 . 2  |-  ( E. x ( ph  \/  ps )  <->  ( -.  E. x ph  ->  E. x ps ) )
7 df-or 370 . 2  |-  ( ( E. x ph  \/  E. x ps )  <->  ( -.  E. x ph  ->  E. x ps ) )
86, 7bitr4i 252 1  |-  ( E. x ( ph  \/  ps )  <->  ( E. x ph  \/  E. x ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368   A.wal 1367   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-or 370  df-ex 1587
This theorem is referenced by:  19.34  1716  19.44  1897  19.45  1898  rexun  3541  unipr  4109  uniun  4115  unopab  4372  zfpair  4534  dmun  5051  coundi  5344  coundir  5345  kmlem16  8339  vdwapun  14040  usgraedg4  23310  pm10.42  29621
  Copyright terms: Public domain W3C validator