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		nfv	|- F/ z ph
3	2	sb8v	|- ( A. y ph <-> A. z [ z / y ] ph )
4	3	sbcbii	|- ( [. A / x ]. A. y ph <-> [. A / x ]. A. z [ z / y ] ph )
5		sbcal	|- ( [. A / x ]. A. z [ z / y ] ph <-> A. z [. A / x ]. [ z / y ] ph )
6		nfs1v	|- F/ y [ z / y ] ph
7	1 6	nfsbcw	|- F/ y [. A / x ]. [ z / y ] ph
8		nfv	|- F/ z [. A / x ]. ph
9		sbequ12r	|- ( z = y -> ( [ z / y ] ph <-> ph ) )
10	9	sbcbidv	|- ( z = y -> ( [. A / x ]. [ z / y ] ph <-> [. A / x ]. ph ) )
11	7 8 10	cbvalv1	|- ( A. z [. A / x ]. [ z / y ] ph <-> A. y [. A / x ]. ph )
12	4 5 11	3bitri	|- ( [. A / x ]. A. y ph <-> A. y [. A / x ]. ph )