Theorem sbcexfi

Description: Move existential 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	sbcexfi.1	|- F/_ y A
	sbcexfi.2	|- ( [. A / x ]. ph <-> ps )
Assertion	sbcexfi	|- ( [. A / x ]. E. y ph <-> E. y ps )

Proof

Step	Hyp	Ref	Expression
1		sbcexfi.1	|- F/_ y A
2		sbcexfi.2	|- ( [. A / x ]. ph <-> ps )
3	1	sbcexf	|- ( [. A / x ]. E. y ph <-> E. y [. A / x ]. ph )
4	2	exbii	|- ( E. y [. A / x ]. ph <-> E. y ps )
5	3 4	bitri	|- ( [. A / x ]. E. y ph <-> E. y ps )