Theorem spesbc

Description: Existence form of spsbc . (Contributed by Mario Carneiro, 18-Nov-2016)

	Ref	Expression
Assertion	spesbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
2		rspesbca	$$⊢\left(A\in \mathrm{V}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to \exists x\in \mathrm{V}\phi$$
3	1 2	mpancom	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \exists x\in \mathrm{V}\phi$$
4		rexv	$$⊢\exists x\in \mathrm{V}\phi \leftrightarrow \exists x\phi$$
5	3 4	sylib	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \exists x\phi$$