Theorem eqrelriv

Description: Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012)

	Ref	Expression
Hypothesis	eqrelriv.1	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
Assertion	eqrelriv	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqrelriv.1	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
2	1	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
3		eqrel	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
4	2 3	mpbiri	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → 𝐴 = 𝐵 )