This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elopaba

Description: Membership in an ordered-pair class abstraction. (Contributed by NM, 25-Feb-2014) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Hypothesis	copsex2ga.1	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
	Assertion	elopaba	$⊢ A \in \{⟨x, y⟩ \| ψ\} \leftrightarrow (A \in (V \times V) \land φ)$

Step	Hyp	Ref	Expression
1		copsex2ga.1	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
2		elopab	$⊢ A \in \{⟨x, y⟩ \| ψ\} \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land ψ)$
3	1	copsex2gb	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land ψ) \leftrightarrow (A \in (V \times V) \land φ)$
4	2 3	bitri	$⊢ A \in \{⟨x, y⟩ \| ψ\} \leftrightarrow (A \in (V \times V) \land φ)$