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

Metamath Proof Explorer

Theorem spcev

Description: Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993) (Proof shortened by Eric Schmidt, 22-Dec-2006)

	Ref	Expression
Hypotheses	spcv.1	$⊢ A \in V$
	spcv.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
Assertion	spcev	$⊢ ψ \to \exists x φ$

Proof

Step	Hyp	Ref	Expression
1		spcv.1	$⊢ A \in V$
2		spcv.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
3	2	spcegv	$⊢ A \in V \to (ψ \to \exists x φ)$
4	1 3	ax-mp	$⊢ ψ \to \exists x φ$