This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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