Theorem r19.42v

Description: Restricted quantifier version of 19.42v (see also 19.42 ). (Contributed by NM, 27-May-1998)

	Ref	Expression
Assertion	r19.42v	$$⊢\exists x\in A\left(\phi \wedge \psi \right)\leftrightarrow \left(\phi \wedge \exists x\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		r19.41v	$$⊢\exists x\in A\left(\psi \wedge \phi \right)\leftrightarrow \left(\exists x\in A\psi \wedge \phi \right)$$
2		ancom	$$⊢\left(\phi \wedge \psi \right)\leftrightarrow \left(\psi \wedge \phi \right)$$
3	2	rexbii	$$⊢\exists x\in A\left(\phi \wedge \psi \right)\leftrightarrow \exists x\in A\left(\psi \wedge \phi \right)$$
4		ancom	$$⊢\left(\phi \wedge \exists x\in A\psi \right)\leftrightarrow \left(\exists x\in A\psi \wedge \phi \right)$$
5	1 3 4	3bitr4i	$$⊢\exists x\in A\left(\phi \wedge \psi \right)\leftrightarrow \left(\phi \wedge \exists x\in A\psi \right)$$