cbvoprab2

Description: Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 11-Dec-2016)

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

Proof

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

Metamath Proof Explorer

Theorem cbvoprab2

Proof