spcgft

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

Step	Hyp	Ref	Expression
1		spcimgfi1.1	$⊢ Ⅎ x ψ$
2		spcimgfi1.2	$⊢ \underline{Ⅎ} x A$
3		biimp	$⊢ (φ \leftrightarrow ψ) \to (φ \to ψ)$
4	3	imim2i	$⊢ (x = A \to (φ \leftrightarrow ψ)) \to (x = A \to (φ \to ψ))$
5	4	alimi	$⊢ \forall x (x = A \to (φ \leftrightarrow ψ)) \to \forall x (x = A \to (φ \to ψ))$
6	1 2	spcimgfi1	$⊢ \forall x (x = A \to (φ \to ψ)) \to (A \in B \to (\forall x φ \to ψ))$
7	5 6	syl	$⊢ \forall x (x = A \to (φ \leftrightarrow ψ)) \to (A \in B \to (\forall x φ \to ψ))$

Metamath Proof Explorer