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		anass	$⊢ ((x \in A \land φ) \land ψ) \leftrightarrow (x \in A \land (φ \land ψ))$
2	1	exbii	$⊢ \exists x ((x \in A \land φ) \land ψ) \leftrightarrow \exists x (x \in A \land (φ \land ψ))$
3		19.41v	$⊢ \exists x ((x \in A \land φ) \land ψ) \leftrightarrow (\exists x (x \in A \land φ) \land ψ)$
4	2 3	bitr3i	$⊢ \exists x (x \in A \land (φ \land ψ)) \leftrightarrow (\exists x (x \in A \land φ) \land ψ)$
5		df-rex	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow \exists x (x \in A \land (φ \land ψ))$
6		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
7	6	anbi1i	$⊢ (\exists x \in A φ \land ψ) \leftrightarrow (\exists x (x \in A \land φ) \land ψ)$
8	4 5 7	3bitr4i	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow (\exists x \in A φ \land ψ)$