Theorem eqbrriv

Description: Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006)

	Ref	Expression
Hypotheses	eqbrriv.1	⊢ Rel 𝐴
	eqbrriv.2	⊢ Rel 𝐵
	eqbrriv.3	⊢ ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 )
Assertion	eqbrriv	⊢ 𝐴 = 𝐵

Proof

Step	Hyp	Ref	Expression
1		eqbrriv.1	⊢ Rel 𝐴
2		eqbrriv.2	⊢ Rel 𝐵
3		eqbrriv.3	⊢ ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 )
4		df-br	⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
5		df-br	⊢ ( 𝑥 𝐵 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
6	3 4 5	3bitr3i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
7	1 2 6	eqrelriiv	⊢ 𝐴 = 𝐵