Theorem cbv2h

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 11-May-1993) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbv2h.1	|- ( ph -> ( ps -> A. y ps ) )
	cbv2h.2	|- ( ph -> ( ch -> A. x ch ) )
	cbv2h.3	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
Assertion	cbv2h	|- ( A. x A. y ph -> ( A. x ps <-> A. y ch ) )

Proof

Step	Hyp	Ref	Expression
1		cbv2h.1	|- ( ph -> ( ps -> A. y ps ) )
2		cbv2h.2	|- ( ph -> ( ch -> A. x ch ) )
3		cbv2h.3	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
4		biimp	|- ( ( ps <-> ch ) -> ( ps -> ch ) )
5	3 4	syl6	|- ( ph -> ( x = y -> ( ps -> ch ) ) )
6	1 2 5	cbv1h	|- ( A. x A. y ph -> ( A. x ps -> A. y ch ) )
7		equcomi	|- ( y = x -> x = y )
8		biimpr	|- ( ( ps <-> ch ) -> ( ch -> ps ) )
9	7 3 8	syl56	|- ( ph -> ( y = x -> ( ch -> ps ) ) )
10	2 1 9	cbv1h	|- ( A. y A. x ph -> ( A. y ch -> A. x ps ) )
11	10	alcoms	|- ( A. x A. y ph -> ( A. y ch -> A. x ps ) )
12	6 11	impbid	|- ( A. x A. y ph -> ( A. x ps <-> A. y ch ) )