Theorem eqbrriv

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

	Ref	Expression
Hypotheses	eqbrriv.1	$$⊢\mathrm{Rel}A$$
	eqbrriv.2	$$⊢\mathrm{Rel}B$$
	eqbrriv.3	$$⊢xAy\leftrightarrow xBy$$
Assertion	eqbrriv	$$⊢A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqbrriv.1	$$⊢\mathrm{Rel}A$$
2		eqbrriv.2	$$⊢\mathrm{Rel}B$$
3		eqbrriv.3	$$⊢xAy\leftrightarrow xBy$$
4		df-br	$$⊢xAy\leftrightarrow ⟨x,y⟩\in A$$
5		df-br	$$⊢xBy\leftrightarrow ⟨x,y⟩\in B$$
6	3 4 5	3bitr3i	$$⊢⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B$$
7	1 2 6	eqrelriiv	$$⊢A=B$$