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 ( 𝑥 = 𝑦𝐴 = 𝐵 )
eqer.2 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝐴 = 𝐵 }
Assertion eqer 𝑅 Er V

Proof

Step Hyp Ref Expression
1 eqer.1 ( 𝑥 = 𝑦𝐴 = 𝐵 )
2 eqer.2 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝐴 = 𝐵 }
3 2 relopabiv Rel 𝑅
4 id ( 𝑧 / 𝑥 𝐴 = 𝑤 / 𝑥 𝐴 𝑧 / 𝑥 𝐴 = 𝑤 / 𝑥 𝐴 )
5 4 eqcomd ( 𝑧 / 𝑥 𝐴 = 𝑤 / 𝑥 𝐴 𝑤 / 𝑥 𝐴 = 𝑧 / 𝑥 𝐴 )
6 1 2 eqerlem ( 𝑧 𝑅 𝑤 𝑧 / 𝑥 𝐴 = 𝑤 / 𝑥 𝐴 )
7 1 2 eqerlem ( 𝑤 𝑅 𝑧 𝑤 / 𝑥 𝐴 = 𝑧 / 𝑥 𝐴 )
8 5 6 7 3imtr4i ( 𝑧 𝑅 𝑤𝑤 𝑅 𝑧 )
9 eqtr ( ( 𝑧 / 𝑥 𝐴 = 𝑤 / 𝑥 𝐴 𝑤 / 𝑥 𝐴 = 𝑣 / 𝑥 𝐴 ) → 𝑧 / 𝑥 𝐴 = 𝑣 / 𝑥 𝐴 )
10 1 2 eqerlem ( 𝑤 𝑅 𝑣 𝑤 / 𝑥 𝐴 = 𝑣 / 𝑥 𝐴 )
11 6 10 anbi12i ( ( 𝑧 𝑅 𝑤𝑤 𝑅 𝑣 ) ↔ ( 𝑧 / 𝑥 𝐴 = 𝑤 / 𝑥 𝐴 𝑤 / 𝑥 𝐴 = 𝑣 / 𝑥 𝐴 ) )
12 1 2 eqerlem ( 𝑧 𝑅 𝑣 𝑧 / 𝑥 𝐴 = 𝑣 / 𝑥 𝐴 )
13 9 11 12 3imtr4i ( ( 𝑧 𝑅 𝑤𝑤 𝑅 𝑣 ) → 𝑧 𝑅 𝑣 )
14 vex 𝑧 ∈ V
15 eqid 𝑧 / 𝑥 𝐴 = 𝑧 / 𝑥 𝐴
16 1 2 eqerlem ( 𝑧 𝑅 𝑧 𝑧 / 𝑥 𝐴 = 𝑧 / 𝑥 𝐴 )
17 15 16 mpbir 𝑧 𝑅 𝑧
18 14 17 2th ( 𝑧 ∈ V ↔ 𝑧 𝑅 𝑧 )
19 3 8 13 18 iseri 𝑅 Er V