Description: Axiom of Quantified Negation. This axiom is used to manipulate negated quantifiers. Equivalent to axiom scheme C7' in Megill p. 448 (p. 16 of the preprint). An alternate axiomatization could use axc5c711 in place of ax-c5 , ax-c7 , and ax-11 .
This axiom is obsolete and should no longer be used. It is proved above as theorem axc7 . (Contributed by NM, 10-Jan-1993) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-c7 | ⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | wph | ⊢ 𝜑 | |
| 2 | 1 0 | wal | ⊢ ∀ 𝑥 𝜑 |
| 3 | 2 | wn | ⊢ ¬ ∀ 𝑥 𝜑 |
| 4 | 3 0 | wal | ⊢ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 |
| 5 | 4 | wn | ⊢ ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 |
| 6 | 5 1 | wi | ⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → 𝜑 ) |