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

Metamath Proof Explorer

Theorem spcegf

Description: Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997)

Ref Expression
Hypotheses spcgf.1 ⊢ Ⅎ _ x A
spcgf.2 ⊢ Ⅎ x ψ
spcgf.3 ⊢ x = A → φ ↔ ψ
Assertion spcegf ⊢ A ∈ V → ψ → ∃ x φ

Proof

Step Hyp Ref Expression
1 spcgf.1 ⊢ Ⅎ _ x A
2 spcgf.2 ⊢ Ⅎ x ψ
3 spcgf.3 ⊢ x = A → φ ↔ ψ
4 2 nfn ⊢ Ⅎ x ¬ ψ
5 3 notbid ⊢ x = A → ¬ φ ↔ ¬ ψ
6 1 4 5 spcgf ⊢ A ∈ V → ∀ x ¬ φ → ¬ ψ
7 6 con2d ⊢ A ∈ V → ψ → ¬ ∀ x ¬ φ
8 df-ex ⊢ ∃ x φ ↔ ¬ ∀ x ¬ φ
9 7 8 imbitrrdi ⊢ A ∈ V → ψ → ∃ x φ