Metamath Proof Explorer

Theorem spcimgfi1OLD

Description: Obsolete version of spcimgfi1 as of 27-Jul-2025. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	spcimgfi1.1	$⊢ Ⅎ x ψ$
		spcimgfi1.2	$⊢ \underline{Ⅎ} x A$
	Assertion	spcimgfi1OLD	$⊢ \forall x (x = A \to (φ \to ψ)) \to (A \in B \to (\forall x φ \to ψ))$

Proof

Step	Hyp	Ref	Expression
1		spcimgfi1.1	$⊢ Ⅎ x ψ$
2		spcimgfi1.2	$⊢ \underline{Ⅎ} x A$
3		elex	$⊢ A \in B \to A \in V$
4	2	issetf	$⊢ A \in V \leftrightarrow \exists x x = A$
5		exim	$⊢ \forall x (x = A \to (φ \to ψ)) \to (\exists x x = A \to \exists x (φ \to ψ))$
6	4 5	biimtrid	$⊢ \forall x (x = A \to (φ \to ψ)) \to (A \in V \to \exists x (φ \to ψ))$
7	1	19.36	$⊢ \exists x (φ \to ψ) \leftrightarrow (\forall x φ \to ψ)$
8	6 7	imbitrdi	$⊢ \forall x (x = A \to (φ \to ψ)) \to (A \in V \to (\forall x φ \to ψ))$
9	3 8	syl5	$⊢ \forall x (x = A \to (φ \to ψ)) \to (A \in B \to (\forall x φ \to ψ))$