Theorem 19.43 1088

Description: Theorem 19.43 of [Margaris] p. 90.

Assertion

Ref	Expression
19.43	|- (E.x(ph \/ ps) <-> (E.xph \/ E.xps))

Proof of Theorem 19.43

Step	Hyp	Ref	Expression
1		ioran 306	. . . . 5 |- (-. (ph \/ ps) <-> (-. ph /\ -. ps))
2	1	albii 999	. . . 4 |- (A.x -. (ph \/ ps) <-> A.x(-. ph /\ -. ps))
3		19.26 1067	. . . 4 |- (A.x(-. ph /\ -. ps) <-> (A.x -. ph /\ A.x -. ps))
4		alnex 1033	. . . . 5 |- (A.x -. ph <-> -. E.xph)
5		alnex 1033	. . . . 5 |- (A.x -. ps <-> -. E.xps)
6	4, 5	anbi12i 482	. . . 4 |- ((A.x -. ph /\ A.x -. ps) <-> (-. E.xph /\ -. E.xps))
7	2, 3, 6	3bitr 177	. . 3 |- (A.x -. (ph \/ ps) <-> (-. E.xph /\ -. E.xps))
8	7	negbii 187	. 2 |- (-. A.x -. (ph \/ ps) <-> -. (-. E.xph /\ -. E.xps))
9		df-ex 981	. 2 |- (E.x(ph \/ ps) <-> -. A.x -. (ph \/ ps))
10		oran 312	. 2 |- ((E.xph \/ E.xps) <-> -. (-. E.xph /\ -. E.xps))
11	8, 9, 10	3bitr4 183	1 |- (E.x(ph \/ ps) <-> (E.xph \/ E.xps))

Syntax hints:  -. wn 2   <-> wb 146   \/ wo 222   /\ wa 223  A.wal 954  E.wex 980

This theorem is referenced by:  19.44 1089  19.45 1090  19.34 1093  euor2 1437  r19.43 1765  unipr 2515  uniun 2519  iunxun 2614  unopab 2679  zfpair 2777  dmun 3317  oarec 4196  kmlem16 4780

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981

Copyright terms: Public domain