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 ∈ 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