Theorem eqbrrdv2

Description: Other version of eqbrrdiv . (Contributed by Rodolfo Medina, 30-Sep-2010)

	Ref	Expression
Hypothesis	eqbrrdv2.1	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 ) )
Assertion	eqbrrdv2	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqbrrdv2.1	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 ) )
2		df-br	⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
3		df-br	⊢ ( 𝑥 𝐵 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
4	1 2 3	3bitr3g	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
5	4	eqrelrdv2	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) ) → 𝐴 = 𝐵 )
6	5	anabss5	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → 𝐴 = 𝐵 )