Metamath Proof Explorer

Theorem spcimgft

Description: Closed theorem form of spcimgf . (Contributed by Wolf Lammen, 28-Jul-2025)

Ref Expression
Assertion spcimgft ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ → ψ → A ∈ V → ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 elissetv ⊢ A ∈ V → ∃ y y = A
2 cbvexeqsetf ⊢ Ⅎ _ x A → ∃ x x = A ↔ ∃ y y = A
3 1 2 imbitrrid ⊢ Ⅎ _ x A → A ∈ V → ∃ x x = A
4 pm2.04 ⊢ x = A → φ → ψ → φ → x = A → ψ
5 4 al2imi ⊢ ∀ x x = A → φ → ψ → ∀ x φ → ∀ x x = A → ψ
6 19.23t ⊢ Ⅎ x ψ → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
7 6 biimpd ⊢ Ⅎ x ψ → ∀ x x = A → ψ → ∃ x x = A → ψ
8 5 7 sylan9r ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ → ψ → ∀ x φ → ∃ x x = A → ψ
9 8 com23 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ → ψ → ∃ x x = A → ∀ x φ → ψ
10 3 9 sylan9 ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ → ψ → A ∈ V → ∀ x φ → ψ
11 10 anassrs ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ → ψ → A ∈ V → ∀ x φ → ψ