Theorem sbcalfi

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

	Ref	Expression
Hypotheses	sbcalfi.1	|- F/_ y A
	sbcalfi.2	|- ( [. A / x ]. ph <-> ps )
Assertion	sbcalfi	|- ( [. A / x ]. A. y ph <-> A. y ps )

Proof

Step	Hyp	Ref	Expression
1		sbcalfi.1	|- F/_ y A
2		sbcalfi.2	|- ( [. A / x ]. ph <-> ps )
3	1	sbcalf	|- ( [. A / x ]. A. y ph <-> A. y [. A / x ]. ph )
4	2	albii	|- ( A. y [. A / x ]. ph <-> A. y ps )
5	3 4	bitri	|- ( [. A / x ]. A. y ph <-> A. y ps )