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

Metamath Proof Explorer

Theorem spcegv

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 25-Aug-2023)

		Ref	Expression
	Hypothesis	spcgv.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	Assertion	spcegv	$⊢ A \in V \to (ψ \to \exists x φ)$

Proof

Step	Hyp	Ref	Expression
1		spcgv.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		elisset	$⊢ A \in V \to \exists x x = A$
3	1	biimprcd	$⊢ ψ \to (x = A \to φ)$
4	3	eximdv	$⊢ ψ \to (\exists x x = A \to \exists x φ)$
5	2 4	syl5com	$⊢ A \in V \to (ψ \to \exists x φ)$