cbvopab

Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003)

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

Proof

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

Metamath Proof Explorer

Theorem cbvopab

Proof