Theorem rspct

Description: A closed version of rspc . (Contributed by Andrew Salmon, 6-Jun-2011)

	Ref	Expression
Hypothesis	rspct.1	⊢ Ⅎ 𝑥 𝜓
Assertion	rspct	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rspct.1	⊢ Ⅎ 𝑥 𝜓
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) )
3		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
4	3	adantr	⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝜑 ↔ 𝜓 ) ) → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
5		simpr	⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝜑 ↔ 𝜓 ) ) → ( 𝜑 ↔ 𝜓 ) )
6	4 5	imbi12d	⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝜑 ↔ 𝜓 ) ) → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) )
7	6	ex	⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
8	7	a2i	⊢ ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
9	8	alimi	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ∀ 𝑥 ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
10		nfv	⊢ Ⅎ 𝑥 𝐴 ∈ 𝐵
11	10 1	nfim	⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝐵 → 𝜓 )
12		nfcv	⊢ Ⅎ 𝑥 𝐴
13	11 12	spcgft	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
14	9 13	syl	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
15	2 14	syl7bi	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → ( 𝐴 ∈ 𝐵 → 𝜓 ) ) ) )
16	15	com34	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → 𝜓 ) ) ) )
17	16	pm2.43d	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → 𝜓 ) ) )