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 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 V z R z
19 3 8 13 18 iseri R Er V