Metamath Proof Explorer

Theorem r19.41v

Description: Restricted quantifier version 19.41v . Version of r19.41 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020)

		Ref	Expression
	Assertion	r19.41v	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow (\exists x \in A φ \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		df-rex	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow \exists x (x \in A \land (φ \land ψ))$
2		anass	$⊢ ((x \in A \land φ) \land ψ) \leftrightarrow (x \in A \land (φ \land ψ))$
3	2	exbii	$⊢ \exists x ((x \in A \land φ) \land ψ) \leftrightarrow \exists x (x \in A \land (φ \land ψ))$
4		19.41v	$⊢ \exists x ((x \in A \land φ) \land ψ) \leftrightarrow (\exists x (x \in A \land φ) \land ψ)$
5		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
6	5	bicomi	$⊢ \exists x (x \in A \land φ) \leftrightarrow \exists x \in A φ$
7	4 6	bianbi	$⊢ \exists x ((x \in A \land φ) \land ψ) \leftrightarrow (\exists x \in A φ \land ψ)$
8	1 3 7	3bitr2i	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow (\exists x \in A φ \land ψ)$