Metamath Proof Explorer

Theorem r19.41

Description: Restricted quantifier version of 19.41 . See r19.41v for a version with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010)

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

Proof

Step	Hyp	Ref	Expression
1		r19.41.1	$⊢ Ⅎ x ψ$
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	1	19.41	$⊢ \exists x ((x \in A \land φ) \land ψ) \leftrightarrow (\exists x (x \in A \land φ) \land ψ)$
5	3 4	bitr3i	$⊢ \exists x (x \in A \land (φ \land ψ)) \leftrightarrow (\exists x (x \in A \land φ) \land ψ)$
6		df-rex	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow \exists x (x \in A \land (φ \land ψ))$
7		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
8	7	anbi1i	$⊢ (\exists x \in A φ \land ψ) \leftrightarrow (\exists x (x \in A \land φ) \land ψ)$
9	5 6 8	3bitr4i	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow (\exists x \in A φ \land ψ)$