Nearby theorems
|
|
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > NFE Home > Th. List > ax-6o | Unicode version | ||
| Description: Axiom of Quantified
Negation. This axiom is used to manipulate negated
quantifiers. One of the 4 axioms of pure predicate calculus. Equivalent
to axiom scheme C7' in [Megill] p. 448 (p.
16 of the preprint). An
alternate axiomatization could use ax467 2169 in place of ax-4 2135,
ax-6o 2137,
and ax-7 1734.
This axiom is obsolete and should no longer be used. It is proved above as Theorem ax6o 1750. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ax-6o |
    
   |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. . . . . 6
 | |
| 2 | vx |
. . . . . 6
 | |
| 3 | 1, 2 | wal 1540 |
. . . . 5
|
| 4 | 3 | wn 3 |
. . . 4
|
| 5 | 4, 2 | wal 1540 |
. . 3
|
| 6 | 5 | wn 3 |
. 2
|
| 7 | 6, 1 | wi 4 |
1
|
| Colors of variables: wff setvar class |
| This axiom is referenced by: ax6 2147 ax9from9o 2148 equid1 2158 ax46 2162 ax67 2165 ax467 2169 equid1ALT 2176 |
| Copyright terms: Public domain | W3C validator |