Theorem spcimedv

Description: Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	spcimdv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	spcimedv.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜒 → 𝜓 ) )
Assertion	spcimedv	⊢ ( 𝜑 → ( 𝜒 → ∃ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		spcimdv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
2		spcimedv.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜒 → 𝜓 ) )
3	2	con3d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ¬ 𝜓 → ¬ 𝜒 ) )
4	1 3	spcimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ¬ 𝜓 → ¬ 𝜒 ) )
5	4	con2d	⊢ ( 𝜑 → ( 𝜒 → ¬ ∀ 𝑥 ¬ 𝜓 ) )
6		df-ex	⊢ ( ∃ 𝑥 𝜓 ↔ ¬ ∀ 𝑥 ¬ 𝜓 )
7	5 6	imbitrrdi	⊢ ( 𝜑 → ( 𝜒 → ∃ 𝑥 𝜓 ) )