Metamath Proof Explorer


Theorem eximal

Description: An equivalence between an implication with an existentially quantified antecedent and an implication with a universally quantified consequent. 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 alimex . (Contributed by BJ, 12-May-2019)

Ref Expression
Assertion eximal xφψ¬ψx¬φ

Proof

Step Hyp Ref Expression
1 df-ex xφ¬x¬φ
2 1 imbi1i xφψ¬x¬φψ
3 con1b ¬x¬φψ¬ψx¬φ
4 2 3 bitri xφψ¬ψx¬φ