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	$$⊢Ⅎx\psi$$
	spcimgfi1.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	spcimgfi1	$$⊢\forall x\left(x=A\to \left(\phi \to \psi \right)\right)\to \left(A\in B\to \left(\forall x\phi \to \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		spcimgfi1.1	$$⊢Ⅎx\psi$$
2		spcimgfi1.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		spcimgft	$$⊢\left(\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\wedge \forall x\left(x=A\to \left(\phi \to \psi \right)\right)\right)\to \left(A\in B\to \left(\forall x\phi \to \psi \right)\right)$$
4	3	ex	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\to \left(\forall x\left(x=A\to \left(\phi \to \psi \right)\right)\to \left(A\in B\to \left(\forall x\phi \to \psi \right)\right)\right)$$
5	2 1 4	mp2an	$$⊢\forall x\left(x=A\to \left(\phi \to \psi \right)\right)\to \left(A\in B\to \left(\forall x\phi \to \psi \right)\right)$$