Theorem cbvralfw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf with a disjoint variable condition, which does not require ax-10 , ax-13 . For a version not dependent on ax-11 and ax-12, see cbvralvw . (Contributed by NM, 7-Mar-2004) Avoid ax-10 , ax-13 . (Revised by GG, 23-May-2024)

	Ref	Expression
Hypotheses	cbvralfw.1	|- F/_ x A
	cbvralfw.2	|- F/_ y A
	cbvralfw.3	|- F/ y ph
	cbvralfw.4	|- F/ x ps
	cbvralfw.5	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvralfw	|- ( A. x e. A ph <-> A. y e. A ps )

Proof

Step	Hyp	Ref	Expression
1		cbvralfw.1	|- F/_ x A
2		cbvralfw.2	|- F/_ y A
3		cbvralfw.3	|- F/ y ph
4		cbvralfw.4	|- F/ x ps
5		cbvralfw.5	|- ( x = y -> ( ph <-> ps ) )
6	2	nfcri	|- F/ y x e. A
7	6 3	nfim	|- F/ y ( x e. A -> ph )
8	1	nfcri	|- F/ x y e. A
9	8 4	nfim	|- F/ x ( y e. A -> ps )
10		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
11	10 5	imbi12d	|- ( x = y -> ( ( x e. A -> ph ) <-> ( y e. A -> ps ) ) )
12	7 9 11	cbvalv1	|- ( A. x ( x e. A -> ph ) <-> A. y ( y e. A -> ps ) )
13		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
14		df-ral	|- ( A. y e. A ps <-> A. y ( y e. A -> ps ) )
15	12 13 14	3bitr4i	|- ( A. x e. A ph <-> A. y e. A ps )