Theorem opabbi2dv

Description: Deduce equality of a relation and an ordered-pair class abstraction. Compare eqabdv . (Contributed by NM, 24-Feb-2014)

	Ref	Expression
Hypotheses	opabbi2dv.1	$$⊢\mathrm{Rel}A$$
	opabbi2dv.3	$$⊢\phi \to \left(⟨x,y⟩\in A\leftrightarrow \psi \right)$$
Assertion	opabbi2dv	$$⊢\phi \to A=\left\{⟨x,y⟩|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		opabbi2dv.1	$$⊢\mathrm{Rel}A$$
2		opabbi2dv.3	$$⊢\phi \to \left(⟨x,y⟩\in A\leftrightarrow \psi \right)$$
3		opabid2	$$⊢\mathrm{Rel}A\to \left\{⟨x,y⟩|⟨x,y⟩\in A\right\}=A$$
4	1 3	ax-mp	$$⊢\left\{⟨x,y⟩|⟨x,y⟩\in A\right\}=A$$
5	2	opabbidv	$$⊢\phi \to \left\{⟨x,y⟩|⟨x,y⟩\in A\right\}=\left\{⟨x,y⟩|\psi \right\}$$
6	4 5	eqtr3id	$$⊢\phi \to A=\left\{⟨x,y⟩|\psi \right\}$$