Description: Theorem *10.253 in WhiteheadRussell p. 149. (Contributed by Andrew Salmon, 17-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | pm10.253 | ⊢ ( ¬ ∀ 𝑥 𝜑 ↔ ∃ 𝑥 ¬ 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alex | ⊢ ( ∀ 𝑥 𝜑 ↔ ¬ ∃ 𝑥 ¬ 𝜑 ) | |
2 | 1 | bicomi | ⊢ ( ¬ ∃ 𝑥 ¬ 𝜑 ↔ ∀ 𝑥 𝜑 ) |
3 | 2 | con1bii | ⊢ ( ¬ ∀ 𝑥 𝜑 ↔ ∃ 𝑥 ¬ 𝜑 ) |