Theorem 19.43 1084

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 996	. . . 4 |- (A.x -. (ph \/ ps) <-> A.x(-. ph /\ -. ps))
3		19.26 1063	. . . 4 |- (A.x(-. ph /\ -. ps) <-> (A.x -. ph /\ A.x -. ps))
4		alnex 1029	. . . . 5 |- (A.x -. ph <-> -. E.xph)
5		alnex 1029	. . . . 5 |- (A.x -. ps <-> -. E.xps)
6	4, 5	anbi12i 481	. . . 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 978	. 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 951  E.wex 977

This theorem is referenced by:  19.44 1085  19.45 1086  19.34 1089  euor2 1430  r19.43 1757  unipr 2505  uniun 2509  iunxun 2604  unopab 2669  zfpair 2767  dmun 3306  oarec 4180  kmlem16 4752

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

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

Copyright terms: Public domain