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

Metamath Proof Explorer

Theorem eqerlem

Description: Lemma for eqer . (Contributed by NM, 17-Mar-2008) (Proof shortened by Mario Carneiro, 6-Dec-2016)

Ref Expression
Hypotheses eqer.1 ⊢ x = y → A = B
eqer.2 ⊢ R = x y | A = B
Assertion eqerlem ⊢ z R w ↔ ⦋ z / x⦌ A = ⦋ w / x⦌ A

Proof

Step Hyp Ref Expression
1 eqer.1 ⊢ x = y → A = B
2 eqer.2 ⊢ R = x y | A = B
3 2 brabsb ⊢ z R w ↔ [˙z / x]˙ [˙w / y]˙ A = B
4 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ A
5 nfcsb1v ⊢ Ⅎ _ x ⦋ w / x⦌ A
6 4 5 nfeq ⊢ Ⅎ x ⦋ z / x⦌ A = ⦋ w / x⦌ A
7 nfv ⊢ Ⅎ y A = ⦋ w / x⦌ A
8 vex ⊢ y ∈ V
9 8 1 csbie ⊢ ⦋ y / x⦌ A = B
10 csbeq1 ⊢ y = w → ⦋ y / x⦌ A = ⦋ w / x⦌ A
11 9 10 eqtr3id ⊢ y = w → B = ⦋ w / x⦌ A
12 11 eqeq2d ⊢ y = w → A = B ↔ A = ⦋ w / x⦌ A
13 7 12 sbciegf ⊢ w ∈ V → [˙w / y]˙ A = B ↔ A = ⦋ w / x⦌ A
14 13 elv ⊢ [˙w / y]˙ A = B ↔ A = ⦋ w / x⦌ A
15 csbeq1a ⊢ x = z → A = ⦋ z / x⦌ A
16 15 eqeq1d ⊢ x = z → A = ⦋ w / x⦌ A ↔ ⦋ z / x⦌ A = ⦋ w / x⦌ A
17 14 16 bitrid ⊢ x = z → [˙w / y]˙ A = B ↔ ⦋ z / x⦌ A = ⦋ w / x⦌ A
18 6 17 sbciegf ⊢ z ∈ V → [˙z / x]˙ [˙w / y]˙ A = B ↔ ⦋ z / x⦌ A = ⦋ w / x⦌ A
19 18 elv ⊢ [˙z / x]˙ [˙w / y]˙ A = B ↔ ⦋ z / x⦌ A = ⦋ w / x⦌ A
20 3 19 bitri ⊢ z R w ↔ ⦋ z / x⦌ A = ⦋ w / x⦌ A