Theorem spcimgfi1 3531

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

Hypotheses

Ref	Expression
spcimgfi1.1	⊢ Ⅎ𝑥𝜓
spcimgfi1.2	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
spcimgfi1	⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓)))

Proof of Theorem spcimgfi1

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-cleq 2728  df-clel 2810  df-nfc 2886

This theorem is referenced by:  spcgft  3533  spcimgf  3534  ss2iundf  43650  spcdvw  49510