elopab

Description: Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998)

		Ref	Expression
	Assertion	elopab	$⊢ A \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)$

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in \{⟨x, y⟩ \| φ\} \to A \in V$
2		opex	$⊢ ⟨x, y⟩ \in V$
3		eleq1	$⊢ A = ⟨x, y⟩ \to (A \in V \leftrightarrow ⟨x, y⟩ \in V)$
4	2 3	mpbiri	$⊢ A = ⟨x, y⟩ \to A \in V$
5	4	adantr	$⊢ (A = ⟨x, y⟩ \land φ) \to A \in V$
6	5	exlimivv	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land φ) \to A \in V$
7		elopabw	$⊢ A \in V \to (A \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ))$
8	1 6 7	pm5.21nii	$⊢ A \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)$

Metamath Proof Explorer