exopxfr2

Description: Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014)

		Ref	Expression
	Hypothesis	exopxfr2.1	$⊢ x = ⟨y, z⟩ \to (φ \leftrightarrow ψ)$
	Assertion	exopxfr2	$⊢ Rel A \to (\exists x \in A φ \leftrightarrow \exists y \exists z (⟨y, z⟩ \in A \land ψ))$

Step	Hyp	Ref	Expression
1		exopxfr2.1	$⊢ x = ⟨y, z⟩ \to (φ \leftrightarrow ψ)$
2		df-rel	$⊢ Rel A \leftrightarrow A \subseteq V \times V$
3	2	biimpi	$⊢ Rel A \to A \subseteq V \times V$
4	3	sseld	$⊢ Rel A \to (x \in A \to x \in (V \times V))$
5	4	adantrd	$⊢ Rel A \to ((x \in A \land φ) \to x \in (V \times V))$
6	5	pm4.71rd	$⊢ Rel A \to ((x \in A \land φ) \leftrightarrow (x \in (V \times V) \land (x \in A \land φ)))$
7	6	rexbidv2	$⊢ Rel A \to (\exists x \in A φ \leftrightarrow \exists x \in (V \times V) (x \in A \land φ))$
8		eleq1	$⊢ x = ⟨y, z⟩ \to (x \in A \leftrightarrow ⟨y, z⟩ \in A)$
9	8 1	anbi12d	$⊢ x = ⟨y, z⟩ \to ((x \in A \land φ) \leftrightarrow (⟨y, z⟩ \in A \land ψ))$
10	9	exopxfr	$⊢ \exists x \in (V \times V) (x \in A \land φ) \leftrightarrow \exists y \exists z (⟨y, z⟩ \in A \land ψ)$
11	7 10	bitrdi	$⊢ Rel A \to (\exists x \in A φ \leftrightarrow \exists y \exists z (⟨y, z⟩ \in A \land ψ))$

Metamath Proof Explorer