spcimgft

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

		Ref	Expression
	Assertion	spcimgft	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land \forall x (x = A \to (φ \to ψ))) \to (A \in V \to (\forall x φ \to ψ))$

Step	Hyp	Ref	Expression
1		elissetv	$⊢ A \in V \to \exists y y = A$
2		cbvexeqsetf	$⊢ \underline{Ⅎ} x A \to (\exists x x = A \leftrightarrow \exists y y = A)$
3	1 2	imbitrrid	$⊢ \underline{Ⅎ} x A \to (A \in V \to \exists x x = A)$
4		pm2.04	$⊢ (x = A \to (φ \to ψ)) \to (φ \to (x = A \to ψ))$
5	4	al2imi	$⊢ \forall x (x = A \to (φ \to ψ)) \to (\forall x φ \to \forall x (x = A \to ψ))$
6		19.23t	$⊢ Ⅎ x ψ \to (\forall x (x = A \to ψ) \leftrightarrow (\exists x x = A \to ψ))$
7	6	biimpd	$⊢ Ⅎ x ψ \to (\forall x (x = A \to ψ) \to (\exists x x = A \to ψ))$
8	5 7	sylan9r	$⊢ (Ⅎ x ψ \land \forall x (x = A \to (φ \to ψ))) \to (\forall x φ \to (\exists x x = A \to ψ))$
9	8	com23	$⊢ (Ⅎ x ψ \land \forall x (x = A \to (φ \to ψ))) \to (\exists x x = A \to (\forall x φ \to ψ))$
10	3 9	sylan9	$⊢ (\underline{Ⅎ} x A \land (Ⅎ x ψ \land \forall x (x = A \to (φ \to ψ)))) \to (A \in V \to (\forall x φ \to ψ))$
11	10	anassrs	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land \forall x (x = A \to (φ \to ψ))) \to (A \in V \to (\forall x φ \to ψ))$

Metamath Proof Explorer