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	imbitrrid	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝜑 → 𝐴 = 𝐵 ) )
5	4	imp	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → 𝐴 = 𝐵 )