Theorem opabid2

Description: A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006)

	Ref	Expression
Assertion	opabid2	⊢ ( Rel 𝐴 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑧 ∈ V
2		vex	⊢ 𝑤 ∈ V
3		opeq1	⊢ ( 𝑥 = 𝑧 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑧 , 𝑦 ⟩ )
4	3	eleq1d	⊢ ( 𝑥 = 𝑧 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ) )
5		opeq2	⊢ ( 𝑦 = 𝑤 → ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
6	5	eleq1d	⊢ ( 𝑦 = 𝑤 → ( ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐴 ) )
7	1 2 4 6	opelopab	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐴 )
8	7	gen2	⊢ ∀ 𝑧 ∀ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐴 )
9		relopabv	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 }
10		eqrel	⊢ ( ( Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } ∧ Rel 𝐴 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = 𝐴 ↔ ∀ 𝑧 ∀ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐴 ) ) )
11	9 10	mpan	⊢ ( Rel 𝐴 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = 𝐴 ↔ ∀ 𝑧 ∀ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐴 ) ) )
12	8 11	mpbiri	⊢ ( Rel 𝐴 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = 𝐴 )