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	⊢ ( 𝑧 𝑅 𝑤 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )