Theorem eqer

Description: Equivalence relation involving equality of dependent classes A ( x ) and B ( y ) . (Contributed by NM, 17-Mar-2008) (Revised by Mario Carneiro, 12-Aug-2015) (Proof shortened by AV, 1-May-2021)

	Ref	Expression
Hypotheses	eqer.1	$$⊢x=y\to A=B$$
	eqer.2	$$⊢R=\left\{⟨x,y⟩|A=B\right\}$$
Assertion	eqer	$$⊢R\mathrm{Er}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		eqer.1	$$⊢x=y\to A=B$$
2		eqer.2	$$⊢R=\left\{⟨x,y⟩|A=B\right\}$$
3	2	relopabi	$$⊢\mathrm{Rel}R$$
4		id	$$⊢⦋z/x⦌A=⦋w/x⦌A\to ⦋z/x⦌A=⦋w/x⦌A$$
5	4	eqcomd	$$⊢⦋z/x⦌A=⦋w/x⦌A\to ⦋w/x⦌A=⦋z/x⦌A$$
6	1 2	eqerlem	$$⊢zRw\leftrightarrow ⦋z/x⦌A=⦋w/x⦌A$$
7	1 2	eqerlem	$$⊢wRz\leftrightarrow ⦋w/x⦌A=⦋z/x⦌A$$
8	5 6 7	3imtr4i	$$⊢zRw\to wRz$$
9		eqtr	$$⊢\left(⦋z/x⦌A=⦋w/x⦌A\wedge ⦋w/x⦌A=⦋v/x⦌A\right)\to ⦋z/x⦌A=⦋v/x⦌A$$
10	1 2	eqerlem	$$⊢wRv\leftrightarrow ⦋w/x⦌A=⦋v/x⦌A$$
11	6 10	anbi12i	$$⊢\left(zRw\wedge wRv\right)\leftrightarrow \left(⦋z/x⦌A=⦋w/x⦌A\wedge ⦋w/x⦌A=⦋v/x⦌A\right)$$
12	1 2	eqerlem	$$⊢zRv\leftrightarrow ⦋z/x⦌A=⦋v/x⦌A$$
13	9 11 12	3imtr4i	$$⊢\left(zRw\wedge wRv\right)\to zRv$$
14		vex	$$⊢z\in \mathrm{V}$$
15		eqid	$$⊢⦋z/x⦌A=⦋z/x⦌A$$
16	1 2	eqerlem	$$⊢zRz\leftrightarrow ⦋z/x⦌A=⦋z/x⦌A$$
17	15 16	mpbir	$$⊢zRz$$
18	14 17	2th	$$⊢z\in \mathrm{V}\leftrightarrow zRz$$
19	3 8 13 18	iseri	$$⊢R\mathrm{Er}\mathrm{V}$$