Metamath Proof Explorer

Theorem pm10.252

Description: Theorem *10.252 in WhiteheadRussell p. 149. (Contributed by Andrew Salmon, 17-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion pm10.252 ( ¬ ∃ 𝑥 𝜑 ↔ ∀ 𝑥 ¬ 𝜑 )

Proof

Step Hyp Ref Expression
1 df-ex ⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )
2 1 bicomi ⊢ ( ¬ ∀ 𝑥 ¬ 𝜑 ↔ ∃ 𝑥 𝜑 )
3 2 con1bii ⊢ ( ¬ ∃ 𝑥 𝜑 ↔ ∀ 𝑥 ¬ 𝜑 )