Theorem cbvopab1

Description: Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004) (Revised by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See cbvopab1g for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvopab1.1	|- F/ z ph
2		cbvopab1.2	|- F/ x ps
3		cbvopab1.3	|- ( x = z -> ( ph <-> ps ) )
4		nfv	|- F/ v E. y ( w = <. x , y >. /\ ph )
5		nfv	|- F/ x w = <. v , y >.
6		nfs1v	|- F/ x [ v / x ] ph
7	5 6	nfan	|- F/ x ( w = <. v , y >. /\ [ v / x ] ph )
8	7	nfex	|- F/ x E. y ( w = <. v , y >. /\ [ v / x ] ph )
9		opeq1	|- ( x = v -> <. x , y >. = <. v , y >. )
10	9	eqeq2d	|- ( x = v -> ( w = <. x , y >. <-> w = <. v , y >. ) )
11		sbequ12	|- ( x = v -> ( ph <-> [ v / x ] ph ) )
12	10 11	anbi12d	|- ( x = v -> ( ( w = <. x , y >. /\ ph ) <-> ( w = <. v , y >. /\ [ v / x ] ph ) ) )
13	12	exbidv	|- ( x = v -> ( E. y ( w = <. x , y >. /\ ph ) <-> E. y ( w = <. v , y >. /\ [ v / x ] ph ) ) )
14	4 8 13	cbvexv1	|- ( E. x E. y ( w = <. x , y >. /\ ph ) <-> E. v E. y ( w = <. v , y >. /\ [ v / x ] ph ) )
15		nfv	|- F/ z w = <. v , y >.
16	1	nfsbv	|- F/ z [ v / x ] ph
17	15 16	nfan	|- F/ z ( w = <. v , y >. /\ [ v / x ] ph )
18	17	nfex	|- F/ z E. y ( w = <. v , y >. /\ [ v / x ] ph )
19		nfv	|- F/ v E. y ( w = <. z , y >. /\ ps )
20		opeq1	|- ( v = z -> <. v , y >. = <. z , y >. )
21	20	eqeq2d	|- ( v = z -> ( w = <. v , y >. <-> w = <. z , y >. ) )
22	2 3	sbhypf	|- ( v = z -> ( [ v / x ] ph <-> ps ) )
23	21 22	anbi12d	|- ( v = z -> ( ( w = <. v , y >. /\ [ v / x ] ph ) <-> ( w = <. z , y >. /\ ps ) ) )
24	23	exbidv	|- ( v = z -> ( E. y ( w = <. v , y >. /\ [ v / x ] ph ) <-> E. y ( w = <. z , y >. /\ ps ) ) )
25	18 19 24	cbvexv1	|- ( E. v E. y ( w = <. v , y >. /\ [ v / x ] ph ) <-> E. z E. y ( w = <. z , y >. /\ ps ) )
26	14 25	bitri	|- ( E. x E. y ( w = <. x , y >. /\ ph ) <-> E. z E. y ( w = <. z , y >. /\ ps ) )
27	26	abbii	|- { w | E. x E. y ( w = <. x , y >. /\ ph ) } = { w | E. z E. y ( w = <. z , y >. /\ ps ) }
28		df-opab	|- { <. x , y >. | ph } = { w | E. x E. y ( w = <. x , y >. /\ ph ) }
29		df-opab	|- { <. z , y >. | ps } = { w | E. z E. y ( w = <. z , y >. /\ ps ) }
30	27 28 29	3eqtr4i	|- { <. x , y >. | ph } = { <. z , y >. | ps }