This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 𝜑 → 𝜓 ) ) )