Theorem 19.45

Description: Theorem 19.45 of Margaris p. 90. See 19.45v for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993)

	Ref	Expression
Hypothesis	19.45.1	|- F/ x ph
Assertion	19.45	|- ( E. x ( ph \/ ps ) <-> ( ph \/ E. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.45.1	|- F/ x ph
2		19.43	|- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) )
3	1	19.9	|- ( E. x ph <-> ph )
4	3	orbi1i	|- ( ( E. x ph \/ E. x ps ) <-> ( ph \/ E. x ps ) )
5	2 4	bitri	|- ( E. x ( ph \/ ps ) <-> ( ph \/ E. x ps ) )