Theorem bj-exim

Description: Theorem 19.22 of Margaris p. 90. (Contributed by NM, 10-Jan-1993) (Proof shortened by Wolf Lammen, 4-Jul-2014) Prove it directly from alim to allow use in bj-alexim . (Revised by BJ, 9-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-exim	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\exists x\phi \to \exists x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		con3	$$⊢\left(\phi \to \psi \right)\to \left(\neg \psi \to \neg \phi \right)$$
2	1	alimi	$$⊢\forall x\left(\phi \to \psi \right)\to \forall x\left(\neg \psi \to \neg \phi \right)$$
3		alim	$$⊢\forall x\left(\neg \psi \to \neg \phi \right)\to \left(\forall x\neg \psi \to \forall x\neg \phi \right)$$
4		con3	$$⊢\left(\forall x\neg \psi \to \forall x\neg \phi \right)\to \left(\neg \forall x\neg \phi \to \neg \forall x\neg \psi \right)$$
5	2 3 4	3syl	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\neg \forall x\neg \phi \to \neg \forall x\neg \psi \right)$$
6		df-ex	$$⊢\exists x\phi \leftrightarrow \neg \forall x\neg \phi$$
7		df-ex	$$⊢\exists x\psi \leftrightarrow \neg \forall x\neg \psi$$
8	5 6 7	3imtr4g	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\exists x\phi \to \exists x\psi \right)$$