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	$$⊢\underset{\_}{Ⅎ}yA$$
	sbcexfi.2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
Assertion	sbcexfi	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\phi \leftrightarrow \exists y\psi$$

Proof

Step	Hyp	Ref	Expression
1		sbcexfi.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		sbcexfi.2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
3	1	sbcexf	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\phi \leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
4	2	exbii	$$⊢\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \exists y\psi$$
5	3 4	bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\phi \leftrightarrow \exists y\psi$$