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 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
eqer.2 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝐴 = 𝐵 }
Assertion eqerlem ( 𝑧 𝑅 𝑤 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )

Proof

Step Hyp Ref Expression
1 eqer.1 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
2 eqer.2 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝐴 = 𝐵 }
3 2 brabsb ⊢ ( 𝑧 𝑅 𝑤 ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝐴 = 𝐵 )
4 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐴
5 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐴
6 4 5 nfeq ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴
7 nfv ⊢ Ⅎ 𝑦 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴
8 vex ⊢ 𝑦 ∈ V
9 8 1 csbie ⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐵
10 csbeq1 ⊢ ( 𝑦 = 𝑤 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
11 9 10 eqtr3id ⊢ ( 𝑦 = 𝑤 → 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
12 11 eqeq2d ⊢ ( 𝑦 = 𝑤 → ( 𝐴 = 𝐵 ↔ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ) )
13 7 12 sbciegf ⊢ ( 𝑤 ∈ V → ( [ 𝑤 / 𝑦 ] 𝐴 = 𝐵 ↔ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ) )
14 13 elv ⊢ ( [ 𝑤 / 𝑦 ] 𝐴 = 𝐵 ↔ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
15 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
16 15 eqeq1d ⊢ ( 𝑥 = 𝑧 → ( 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ) )
17 14 16 bitrid ⊢ ( 𝑥 = 𝑧 → ( [ 𝑤 / 𝑦 ] 𝐴 = 𝐵 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ) )
18 6 17 sbciegf ⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝐴 = 𝐵 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ) )
19 18 elv ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝐴 = 𝐵 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
20 3 19 bitri ⊢ ( 𝑧 𝑅 𝑤 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )