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	|- F/_ x [_ z / x ]_ A
5		nfcsb1v	|- F/_ x [_ w / x ]_ A
6	4 5	nfeq	|- F/ x [_ z / x ]_ A = [_ w / x ]_ A
7		nfv	|- F/ y A = [_ w / x ]_ A
8		vex	|- y e. _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 e. _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 e. _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 )