Metamath Proof Explorer


Theorem eqrelrdv2

Description: A version of eqrelrdv . (Contributed by Rodolfo Medina, 10-Oct-2010)

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

Proof

Step Hyp Ref Expression
1 eqrelrdv2.1 ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
2 1 alrimivv ( 𝜑 → ∀ 𝑥𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
3 eqrel ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
4 2 3 syl5ibr ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝜑𝐴 = 𝐵 ) )
5 4 imp ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → 𝐴 = 𝐵 )