Theorem eqrelrdv

Description: Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010)

	Ref	Expression
Hypotheses	eqrelrdv.1	⊢ Rel 𝐴
	eqrelrdv.2	⊢ Rel 𝐵
	eqrelrdv.3	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
Assertion	eqrelrdv	⊢ ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqrelrdv.1	⊢ Rel 𝐴
2		eqrelrdv.2	⊢ Rel 𝐵
3		eqrelrdv.3	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
4	3	alrimivv	⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
5		eqrel	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
6	1 2 5	mp2an	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
7	4 6	sylibr	⊢ ( 𝜑 → 𝐴 = 𝐵 )