Theorem sbcalf

Description: Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019)

	Ref	Expression
Hypothesis	sbcalf.1	|- F/_ y A
Assertion	sbcalf	|- ( [. A / x ]. A. y ph <-> A. y [. A / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbcalf.1	|- F/_ y A
2		sb8v	|- ( A. y ph <-> A. z [ z / y ] ph )
3	2	sbcbii	|- ( [. A / x ]. A. y ph <-> [. A / x ]. A. z [ z / y ] ph )
4		sbcal	|- ( [. A / x ]. A. z [ z / y ] ph <-> A. z [. A / x ]. [ z / y ] ph )
5		nfs1v	|- F/ y [ z / y ] ph
6	1 5	nfsbcw	|- F/ y [. A / x ]. [ z / y ] ph
7		nfv	|- F/ z [. A / x ]. ph
8		sbequ12r	|- ( z = y -> ( [ z / y ] ph <-> ph ) )
9	8	sbcbidv	|- ( z = y -> ( [. A / x ]. [ z / y ] ph <-> [. A / x ]. ph ) )
10	6 7 9	cbvalv1	|- ( A. z [. A / x ]. [ z / y ] ph <-> A. y [. A / x ]. ph )
11	3 4 10	3bitri	|- ( [. A / x ]. A. y ph <-> A. y [. A / x ]. ph )