Theorem rspc

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005) (Revised by Mario Carneiro, 11-Oct-2016)

	Ref	Expression
Hypotheses	rspc.1	⊢ Ⅎ 𝑥 𝜓
	rspc.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	rspc	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rspc.1	⊢ Ⅎ 𝑥 𝜓
2		rspc.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) )
4		nfcv	⊢ Ⅎ 𝑥 𝐴
5		nfv	⊢ Ⅎ 𝑥 𝐴 ∈ 𝐵
6	5 1	nfim	⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝐵 → 𝜓 )
7		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
8	7 2	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) )
9	4 6 8	spcgf	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝐴 ∈ 𝐵 → 𝜓 ) ) )
10	9	pm2.43a	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) → 𝜓 ) )
11	3 10	syl5bi	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → 𝜓 ) )