This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvoprab1

Description: Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008) (Revised by Mario Carneiro, 5-Dec-2016)

Ref Expression
Hypotheses cbvoprab1.1 
|- F/ w ph
cbvoprab1.2 
|- F/ x ps
cbvoprab1.3 
|- ( x = w -> ( ph <-> ps ) )
Assertion cbvoprab1 
|- { <. <. x , y >. , z >. | ph } = { <. <. w , y >. , z >. | ps }

Proof

Step Hyp Ref Expression
1 cbvoprab1.1 
 |-  F/ w ph
2 cbvoprab1.2 
 |-  F/ x ps
3 cbvoprab1.3 
 |-  ( x = w -> ( ph <-> ps ) )
4 nfv 
 |-  F/ w v = <. x , y >.
5 4 1 nfan 
 |-  F/ w ( v = <. x , y >. /\ ph )
6 5 nfex 
 |-  F/ w E. y ( v = <. x , y >. /\ ph )
7 nfv 
 |-  F/ x v = <. w , y >.
8 7 2 nfan 
 |-  F/ x ( v = <. w , y >. /\ ps )
9 8 nfex 
 |-  F/ x E. y ( v = <. w , y >. /\ ps )
10 opeq1 
 |-  ( x = w -> <. x , y >. = <. w , y >. )
11 10 eqeq2d 
 |-  ( x = w -> ( v = <. x , y >. <-> v = <. w , y >. ) )
12 11 3 anbi12d 
 |-  ( x = w -> ( ( v = <. x , y >. /\ ph ) <-> ( v = <. w , y >. /\ ps ) ) )
13 12 exbidv 
 |-  ( x = w -> ( E. y ( v = <. x , y >. /\ ph ) <-> E. y ( v = <. w , y >. /\ ps ) ) )
14 6 9 13 cbvexv1 
 |-  ( E. x E. y ( v = <. x , y >. /\ ph ) <-> E. w E. y ( v = <. w , y >. /\ ps ) )
15 14 opabbii 
 |-  { <. v , z >. | E. x E. y ( v = <. x , y >. /\ ph ) } = { <. v , z >. | E. w E. y ( v = <. w , y >. /\ ps ) }
16 dfoprab2 
 |-  { <. <. x , y >. , z >. | ph } = { <. v , z >. | E. x E. y ( v = <. x , y >. /\ ph ) }
17 dfoprab2 
 |-  { <. <. w , y >. , z >. | ps } = { <. v , z >. | E. w E. y ( v = <. w , y >. /\ ps ) }
18 15 16 17 3eqtr4i 
 |-  { <. <. x , y >. , z >. | ph } = { <. <. w , y >. , z >. | ps }