Theorem cbv3hv

Description: Rule used to change bound variables, using implicit substitution. Version of cbv3h with a disjoint variable condition on x , y , which does not require ax-13 . Was used in a proof of axc11n (but of independent interest). (Contributed by NM, 25-Jul-2015) (Proof shortened by Wolf Lammen, 29-Nov-2020) (Proof shortened by BJ, 30-Nov-2020)

	Ref	Expression
Hypotheses	cbv3hv.nf1	|- ( ph -> A. y ph )
	cbv3hv.nf2	|- ( ps -> A. x ps )
	cbv3hv.1	|- ( x = y -> ( ph -> ps ) )
Assertion	cbv3hv	|- ( A. x ph -> A. y ps )

Proof

Step	Hyp	Ref	Expression
1		cbv3hv.nf1	|- ( ph -> A. y ph )
2		cbv3hv.nf2	|- ( ps -> A. x ps )
3		cbv3hv.1	|- ( x = y -> ( ph -> ps ) )
4	1	nf5i	|- F/ y ph
5	2	nf5i	|- F/ x ps
6	4 5 3	cbv3v	|- ( A. x ph -> A. y ps )