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 -> A = B )
	eqer.2	|- R = { <. x , y >. | A = B }
Assertion	eqer	|- R Er _V

Proof

Step	Hyp	Ref	Expression
1		eqer.1	|- ( x = y -> A = B )
2		eqer.2	|- R = { <. x , y >. | A = B }
3	2	relopabiv	|- Rel R
4		id	|- ( [_ z / x ]_ A = [_ w / x ]_ A -> [_ z / x ]_ A = [_ w / x ]_ A )
5	4	eqcomd	|- ( [_ z / x ]_ A = [_ w / x ]_ A -> [_ w / x ]_ A = [_ z / x ]_ A )
6	1 2	eqerlem	|- ( z R w <-> [_ z / x ]_ A = [_ w / x ]_ A )
7	1 2	eqerlem	|- ( w R z <-> [_ w / x ]_ A = [_ z / x ]_ A )
8	5 6 7	3imtr4i	|- ( z R w -> w R z )
9		eqtr	|- ( ( [_ z / x ]_ A = [_ w / x ]_ A /\ [_ w / x ]_ A = [_ v / x ]_ A ) -> [_ z / x ]_ A = [_ v / x ]_ A )
10	1 2	eqerlem	|- ( w R v <-> [_ w / x ]_ A = [_ v / x ]_ A )
11	6 10	anbi12i	|- ( ( z R w /\ w R v ) <-> ( [_ z / x ]_ A = [_ w / x ]_ A /\ [_ w / x ]_ A = [_ v / x ]_ A ) )
12	1 2	eqerlem	|- ( z R v <-> [_ z / x ]_ A = [_ v / x ]_ A )
13	9 11 12	3imtr4i	|- ( ( z R w /\ w R v ) -> z R v )
14		vex	|- z e. _V
15		eqid	|- [_ z / x ]_ A = [_ z / x ]_ A
16	1 2	eqerlem	|- ( z R z <-> [_ z / x ]_ A = [_ z / x ]_ A )
17	15 16	mpbir	|- z R z
18	14 17	2th	|- ( z e. _V <-> z R z )
19	3 8 13 18	iseri	|- R Er _V