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\to A=B$$
	eqer.2	$$⊢R=\left\{⟨x,y⟩|A=B\right\}$$
Assertion	eqerlem	$$⊢zRw\leftrightarrow ⦋z/x⦌A=⦋w/x⦌A$$

Proof

Step	Hyp	Ref	Expression
1		eqer.1	$$⊢x=y\to A=B$$
2		eqer.2	$$⊢R=\left\{⟨x,y⟩|A=B\right\}$$
3	2	brabsb	$$⊢zRw\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}A=B$$
4		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌A$$
5		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋w/x⦌A$$
6	4 5	nfeq	$$⊢Ⅎx⦋z/x⦌A=⦋w/x⦌A$$
7		nfv	$$⊢ℲyA=⦋w/x⦌A$$
8		vex	$$⊢y\in \mathrm{V}$$
9	8 1	csbie	$$⊢⦋y/x⦌A=B$$
10		csbeq1	$$⊢y=w\to ⦋y/x⦌A=⦋w/x⦌A$$
11	9 10	eqtr3id	$$⊢y=w\to B=⦋w/x⦌A$$
12	11	eqeq2d	$$⊢y=w\to \left(A=B\leftrightarrow A=⦋w/x⦌A\right)$$
13	7 12	sbciegf	$$⊢w\in \mathrm{V}\to \left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}A=B\leftrightarrow A=⦋w/x⦌A\right)$$
14	13	elv	$$⊢\underset{\dot{}}{[}w/y\underset{\dot{}}{]}A=B\leftrightarrow A=⦋w/x⦌A$$
15		csbeq1a	$$⊢x=z\to A=⦋z/x⦌A$$
16	15	eqeq1d	$$⊢x=z\to \left(A=⦋w/x⦌A\leftrightarrow ⦋z/x⦌A=⦋w/x⦌A\right)$$
17	14 16	bitrid	$$⊢x=z\to \left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}A=B\leftrightarrow ⦋z/x⦌A=⦋w/x⦌A\right)$$
18	6 17	sbciegf	$$⊢z\in \mathrm{V}\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}A=B\leftrightarrow ⦋z/x⦌A=⦋w/x⦌A\right)$$
19	18	elv	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}A=B\leftrightarrow ⦋z/x⦌A=⦋w/x⦌A$$
20	3 19	bitri	$$⊢zRw\leftrightarrow ⦋z/x⦌A=⦋w/x⦌A$$