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	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	Assertion	spcegv	⊢ ( 𝐴 ∈ 𝑉 → ( 𝜓 → ∃ 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		spcgv.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		elisset	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
3	1	biimprcd	⊢ ( 𝜓 → ( 𝑥 = 𝐴 → 𝜑 ) )
4	3	eximdv	⊢ ( 𝜓 → ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 𝜑 ) )
5	2 4	syl5com	⊢ ( 𝐴 ∈ 𝑉 → ( 𝜓 → ∃ 𝑥 𝜑 ) )