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	$⊢ Ⅎ x ψ$
	spcimgfi1.2	$⊢ \underline{Ⅎ} x A$
Assertion	spcimgfi1	$⊢ \forall x (x = A \to (φ \to ψ)) \to (A \in B \to (\forall x φ \to ψ))$

Step	Hyp	Ref	Expression
1		spcimgfi1.1	$⊢ Ⅎ x ψ$
2		spcimgfi1.2	$⊢ \underline{Ⅎ} x A$
3		spcimgft	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land \forall x (x = A \to (φ \to ψ))) \to (A \in B \to (\forall x φ \to ψ))$
4	2 1 3	mpanl12	$⊢ \forall x (x = A \to (φ \to ψ)) \to (A \in B \to (\forall x φ \to ψ))$