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	⊢ Rel 𝐴
	opabbi2dv.3	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ 𝜓 ) )
Assertion	opabbi2dv	⊢ ( 𝜑 → 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		opabbi2dv.1	⊢ Rel 𝐴
2		opabbi2dv.3	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ 𝜓 ) )
3		opabid2	⊢ ( Rel 𝐴 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = 𝐴 )
4	1 3	ax-mp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = 𝐴
5	2	opabbidv	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
6	4 5	eqtr3id	⊢ ( 𝜑 → 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )