Theorem rspcimedv

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

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

Proof

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