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 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
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