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 
 |-  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 )