Metamath Proof Explorer

Theorem rexbidv2

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999)

		Ref	Expression
	Hypothesis	rexbidv2.1	$⊢ φ \to ((x \in A \land ψ) \leftrightarrow (x \in B \land χ))$
	Assertion	rexbidv2	$⊢ φ \to (\exists x \in A ψ \leftrightarrow \exists x \in B χ)$

Step	Hyp	Ref	Expression
1		rexbidv2.1	$⊢ φ \to ((x \in A \land ψ) \leftrightarrow (x \in B \land χ))$
2	1	exbidv	$⊢ φ \to (\exists x (x \in A \land ψ) \leftrightarrow \exists x (x \in B \land χ))$
3		df-rex	$⊢ \exists x \in A ψ \leftrightarrow \exists x (x \in A \land ψ)$
4		df-rex	$⊢ \exists x \in B χ \leftrightarrow \exists x (x \in B \land χ)$
5	2 3 4	3bitr4g	$⊢ φ \to (\exists x \in A ψ \leftrightarrow \exists x \in B χ)$