Metamath Proof Explorer

Theorem bj-spim

Description: A lemma for universal specification. In applications, x = y will be substituted for ps and ax6ev will prove Hypothesis bj-spim.denote. (Contributed by BJ, 4-Apr-2026)

		Ref	Expression
	Hypotheses	bj-spim.nf0	$⊢ φ \to \forall x φ$
		bj-spim.nf	$⊢ φ \to (\exists x θ \to θ)$
		bj-spim.denote	$⊢ φ \to \exists x ψ$
		bj-spim.maj	$⊢ (φ \land ψ) \to (χ \to θ)$
	Assertion	bj-spim	$⊢ φ \to (\forall x χ \to θ)$

Proof

Step	Hyp	Ref	Expression
1		bj-spim.nf0	$⊢ φ \to \forall x φ$
2		bj-spim.nf	$⊢ φ \to (\exists x θ \to θ)$
3		bj-spim.denote	$⊢ φ \to \exists x ψ$
4		bj-spim.maj	$⊢ (φ \land ψ) \to (χ \to θ)$
5	4	ex	$⊢ φ \to (ψ \to (χ \to θ))$
6	1 5	eximdh	$⊢ φ \to (\exists x ψ \to \exists x (χ \to θ))$
7	3 6	mpd	$⊢ φ \to \exists x (χ \to θ)$
8		bj-spimnfe	$⊢ (\exists x θ \to θ) \to (\exists x (χ \to θ) \to (\forall x χ \to θ))$
9	2 7 8	sylc	$⊢ φ \to (\forall x χ \to θ)$