Metamath Proof Explorer


Theorem dfrex2

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997) (Proof shortened by Wolf Lammen, 26-Nov-2019)

Ref Expression
Assertion dfrex2 ( ∃ 𝑥𝐴 𝜑 ↔ ¬ ∀ 𝑥𝐴 ¬ 𝜑 )

Proof

Step Hyp Ref Expression
1 ralnex ( ∀ 𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃ 𝑥𝐴 𝜑 )
2 1 con2bii ( ∃ 𝑥𝐴 𝜑 ↔ ¬ ∀ 𝑥𝐴 ¬ 𝜑 )