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		df-rex	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow \exists x (x \in A \land (φ \land ψ))$
3		anass	$⊢ ((x \in A \land φ) \land ψ) \leftrightarrow (x \in A \land (φ \land ψ))$
4	3	exbii	$⊢ \exists x ((x \in A \land φ) \land ψ) \leftrightarrow \exists x (x \in A \land (φ \land ψ))$
5	1	19.41	$⊢ \exists x ((x \in A \land φ) \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	bicomi	$⊢ \exists x (x \in A \land φ) \leftrightarrow \exists x \in A φ$
8	5 7	bianbi	$⊢ \exists x ((x \in A \land φ) \land ψ) \leftrightarrow (\exists x \in A φ \land ψ)$
9	2 4 8	3bitr2i	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow (\exists x \in A φ \land ψ)$