Theorem bj-eximALT

Description: Alternate proof of exim directly from alim by using df-ex (using duality of A. and E. . (Contributed by BJ, 9-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-eximALT	$$⊢\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)$$