Theorem sbcexf

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

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

Proof

Step	Hyp	Ref	Expression
1		sbcexf.1	|- F/_ y A
2		nfv	|- F/ z ph
3	2	sb8ef	|- ( E. y ph <-> E. z [ z / y ] ph )
4	3	sbcbii	|- ( [. A / x ]. E. y ph <-> [. A / x ]. E. z [ z / y ] ph )
5		sbcex2	|- ( [. A / x ]. E. z [ z / y ] ph <-> E. 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	cbvexv1	|- ( E. z [. A / x ]. [ z / y ] ph <-> E. y [. A / x ]. ph )
12	4 5 11	3bitri	|- ( [. A / x ]. E. y ph <-> E. y [. A / x ]. ph )