Theorem r19.43

Description: Restricted quantifier version of 19.43 . (Contributed by NM, 27-May-1998) (Proof shortened by Andrew Salmon, 30-May-2011)

	Ref	Expression
Assertion	r19.43	$$⊢\exists x\in A\left(\phi \vee \psi \right)\leftrightarrow \left(\exists x\in A\phi \vee \exists x\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		r19.35	$$⊢\exists x\in A\left(\neg \phi \to \psi \right)\leftrightarrow \left(\forall x\in A\neg \phi \to \exists x\in A\psi \right)$$
2		df-or	$$⊢\left(\phi \vee \psi \right)\leftrightarrow \left(\neg \phi \to \psi \right)$$
3	2	rexbii	$$⊢\exists x\in A\left(\phi \vee \psi \right)\leftrightarrow \exists x\in A\left(\neg \phi \to \psi \right)$$
4		df-or	$$⊢\left(\exists x\in A\phi \vee \exists x\in A\psi \right)\leftrightarrow \left(\neg \exists x\in A\phi \to \exists x\in A\psi \right)$$
5		ralnex	$$⊢\forall x\in A\neg \phi \leftrightarrow \neg \exists x\in A\phi$$
6	5	imbi1i	$$⊢\left(\forall x\in A\neg \phi \to \exists x\in A\psi \right)\leftrightarrow \left(\neg \exists x\in A\phi \to \exists x\in A\psi \right)$$
7	4 6	bitr4i	$$⊢\left(\exists x\in A\phi \vee \exists x\in A\psi \right)\leftrightarrow \left(\forall x\in A\neg \phi \to \exists x\in A\psi \right)$$
8	1 3 7	3bitr4i	$$⊢\exists x\in A\left(\phi \vee \psi \right)\leftrightarrow \left(\exists x\in A\phi \vee \exists x\in A\psi \right)$$