This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Restricted quantification Restricted universal and existential quantification 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 ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 )