Theorem spcgft

Description: A closed version of spcgf . (Contributed by Andrew Salmon, 6-Jun-2011) (Revised by Mario Carneiro, 4-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		spcimgfi1.1	⊢ Ⅎ 𝑥 𝜓
2		spcimgfi1.2	⊢ Ⅎ 𝑥 𝐴
3		biimp	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜑 → 𝜓 ) )
4	3	imim2i	⊢ ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) ) )
5	4	alimi	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) ) )
6	1 2	spcimgfi1	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 𝜑 → 𝜓 ) ) )
7	5 6	syl	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 𝜑 → 𝜓 ) ) )