Theorem alimex

Description: An equivalence between an implication with a universally quantified consequent and an implication with an existentially quantified antecedent. An interesting case is when the same formula is substituted for both ph and ps , since then both implications express a type of nonfreeness. See also eximal . (Contributed by BJ, 12-May-2019)

	Ref	Expression
Assertion	alimex	$$⊢\left(\phi \to \forall x\psi \right)\leftrightarrow \left(\exists x\neg \psi \to \neg \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		alex	$$⊢\forall x\psi \leftrightarrow \neg \exists x\neg \psi$$
2	1	imbi2i	$$⊢\left(\phi \to \forall x\psi \right)\leftrightarrow \left(\phi \to \neg \exists x\neg \psi \right)$$
3		con2b	$$⊢\left(\phi \to \neg \exists x\neg \psi \right)\leftrightarrow \left(\exists x\neg \psi \to \neg \phi \right)$$
4	2 3	bitri	$$⊢\left(\phi \to \forall x\psi \right)\leftrightarrow \left(\exists x\neg \psi \to \neg \phi \right)$$