Theorem cbvex1v

Description: Rule used to change bound variables, using implicit substitution. (Contributed by BTernaryTau, 31-Jul-2025)

	Ref	Expression
Hypotheses	cbvex1v.1	|- F/ x ph
	cbvex1v.2	|- F/ y ph
	cbvex1v.3	|- ( ph -> F/ y ps )
	cbvex1v.4	|- ( ph -> F/ x ch )
	cbvex1v.5	|- ( ph -> ( x = y -> ( ps -> ch ) ) )
Assertion	cbvex1v	|- ( ph -> ( E. x ps -> E. y ch ) )

Proof

Step	Hyp	Ref	Expression
1		cbvex1v.1	|- F/ x ph
2		cbvex1v.2	|- F/ y ph
3		cbvex1v.3	|- ( ph -> F/ y ps )
4		cbvex1v.4	|- ( ph -> F/ x ch )
5		cbvex1v.5	|- ( ph -> ( x = y -> ( ps -> ch ) ) )
6	4	nfnd	|- ( ph -> F/ x -. ch )
7	3	nfnd	|- ( ph -> F/ y -. ps )
8		equcomi	|- ( y = x -> x = y )
9		con3	|- ( ( ps -> ch ) -> ( -. ch -> -. ps ) )
10	8 5 9	syl56	|- ( ph -> ( y = x -> ( -. ch -> -. ps ) ) )
11	2 1 6 7 10	cbv1v	|- ( ph -> ( A. y -. ch -> A. x -. ps ) )
12	11	con3d	|- ( ph -> ( -. A. x -. ps -> -. A. y -. ch ) )
13		df-ex	|- ( E. x ps <-> -. A. x -. ps )
14		df-ex	|- ( E. y ch <-> -. A. y -. ch )
15	12 13 14	3imtr4g	|- ( ph -> ( E. x ps -> E. y ch ) )