This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem spesbc

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

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

Step	Hyp	Ref	Expression
1		sbcex	$⊢ \underset{˙}{[} A / x \underset{˙}{]} φ \to A \in V$
2		rspesbca	$⊢ (A \in V \land \underset{˙}{[} A / x \underset{˙}{]} φ) \to \exists x \in V φ$
3	1 2	mpancom	$⊢ \underset{˙}{[} A / x \underset{˙}{]} φ \to \exists x \in V φ$
4		rexv	$⊢ \exists x \in V φ \leftrightarrow \exists x φ$
5	3 4	sylib	$⊢ \underset{˙}{[} A / x \underset{˙}{]} φ \to \exists x φ$