Theorem spesbc

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

	Ref	Expression
Assertion	spesbc	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → ∃ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbcex	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
2		rspesbca	⊢ ( ( 𝐴 ∈ V ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → ∃ 𝑥 ∈ V 𝜑 )
3	1 2	mpancom	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → ∃ 𝑥 ∈ V 𝜑 )
4		rexv	⊢ ( ∃ 𝑥 ∈ V 𝜑 ↔ ∃ 𝑥 𝜑 )
5	3 4	sylib	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → ∃ 𝑥 𝜑 )