Nearby theorems
|
|
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-c7 | Structured version Visualization version Unicode version | ||
| 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 34203 in place
of ax-c5 34168, ax-c7 34170, and ax-11 2034.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc7 2132. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ax-c7 |
      
 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. . . . . 6
 | |
| 2 | vx |
. . . . . 6
 | |
| 3 | 1, 2 | wal 1481 |
. . . . 5
|
| 4 | 3 | wn 3 |
. . . 4
|
| 5 | 4, 2 | wal 1481 |
. . 3
|
| 6 | 5 | wn 3 |
. 2
|
| 7 | 6, 1 | wi 4 |
1
|
| Colors of variables: wff setvar class |
| This axiom is referenced by: ax10fromc7 34180 ax6fromc10 34181 equid1 34184 axc5c7 34196 axc711 34199 axc5c711 34203 equid1ALT 34210 |
| Copyright terms: Public domain | W3C validator |