Theorem rspcimdv

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

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

Proof

Step	Hyp	Ref	Expression
1		rspcimdv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
2		rspcimdv.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 → 𝜒 ) )
3		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 𝜓 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜓 ) )
4		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
5	4	eleq1d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
6	5	biimprd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐵 ) )
7	6 2	imim12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝑥 ∈ 𝐵 → 𝜓 ) → ( 𝐴 ∈ 𝐵 → 𝜒 ) ) )
8	1 7	spcimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜓 ) → ( 𝐴 ∈ 𝐵 → 𝜒 ) ) )
9	1 8	mpid	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜓 ) → 𝜒 ) )
10	3 9	syl5bi	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 𝜓 → 𝜒 ) )