Theorem 19.43 1129

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 313	. . . . 5 |- (-. (ph \/ ps) <-> (-. ph /\ -. ps))
2	1	albii 1040	. . . 4 |- (A.x -. (ph \/ ps) <-> A.x(-. ph /\ -. ps))
3		19.26 1108	. . . 4 |- (A.x(-. ph /\ -. ps) <-> (A.x -. ph /\ A.x -. ps))
4		alnex 1074	. . . . 5 |- (A.x -. ph <-> -. E.xph)
5		alnex 1074	. . . . 5 |- (A.x -. ps <-> -. E.xps)
6	4, 5	anbi12i 493	. . . 4 |- ((A.x -. ph /\ A.x -. ps) <-> (-. E.xph /\ -. E.xps))
7	2, 3, 6	3bitri 184	. . 3 |- (A.x -. (ph \/ ps) <-> (-. E.xph /\ -. E.xps))
8	7	notbii 194	. 2 |- (-. A.x -. (ph \/ ps) <-> -. (-. E.xph /\ -. E.xps))
9		df-ex 1022	. 2 |- (E.x(ph \/ ps) <-> -. A.x -. (ph \/ ps))
10		oran 319	. 2 |- ((E.xph \/ E.xps) <-> -. (-. E.xph /\ -. E.xps))
11	8, 9, 10	3bitr4i 190	1 |- (E.x(ph \/ ps) <-> (E.xph \/ E.xps))

Syntax hints:  -. wn 2   <-> wb 153   \/ wo 229   /\ wa 230  A.wal 995  E.wex 1021

This theorem is referenced by:  19.44 1130  19.45 1131  19.34 1134  euor2 1480  r19.43 1812  unipr 2569  uniun 2573  iunxun 2669  unopab 2734  zfpair 2833  dmun 3374  oarec 4254  kmlem16 4842

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022

Copyright terms: Public domain