Theorem spcimgfi1

Description: A closed version of spcimgf . (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by Wolf Lammen, 27-Jul-2025)

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

Proof

Step	Hyp	Ref	Expression
1		spcimgfi1.1	⊢ Ⅎ 𝑥 𝜓
2		spcimgfi1.2	⊢ Ⅎ 𝑥 𝐴
3		spcimgft	⊢ ( ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 𝜑 → 𝜓 ) ) )
4	3	ex	⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 𝜑 → 𝜓 ) ) ) )
5	2 1 4	mp2an	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 𝜑 → 𝜓 ) ) )