New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > ax-12o | GIF version |
Description: Axiom of Quantifier
Introduction. One of the equality and substitution
axioms of predicate calculus with equality. Informally, it says that
whenever z is distinct
from x and y, and x = y is
true,
then x = y quantified with z is also true. In other words, z
is irrelevant to the truth of x
= y. Axiom scheme C9' in [Megill]
p. 448 (p. 16 of the preprint). It apparently does not otherwise appear
in the literature but is easily proved from textbook predicate calculus by
cases.
This axiom is obsolete and should no longer be used. It is proved above as theorem ax12o 1934. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-12o | ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vz | . . . . 5 setvar z | |
2 | vx | . . . . 5 setvar x | |
3 | 1, 2 | weq 1643 | . . . 4 wff z = x |
4 | 3, 1 | wal 1540 | . . 3 wff ∀z z = x |
5 | 4 | wn 3 | . 2 wff ¬ ∀z z = x |
6 | vy | . . . . . 6 setvar y | |
7 | 1, 6 | weq 1643 | . . . . 5 wff z = y |
8 | 7, 1 | wal 1540 | . . . 4 wff ∀z z = y |
9 | 8 | wn 3 | . . 3 wff ¬ ∀z z = y |
10 | 2, 6 | weq 1643 | . . . 4 wff x = y |
11 | 10, 1 | wal 1540 | . . . 4 wff ∀z x = y |
12 | 10, 11 | wi 4 | . . 3 wff (x = y → ∀z x = y) |
13 | 9, 12 | wi 4 | . 2 wff (¬ ∀z z = y → (x = y → ∀z x = y)) |
14 | 5, 13 | wi 4 | 1 wff (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y))) |
Colors of variables: wff setvar class |
This axiom is referenced by: hbae-o 2153 ax12from12o 2156 equid1 2158 hbequid 2160 equid1ALT 2176 dvelimf-o 2180 ax17eq 2183 |
Copyright terms: Public domain | W3C validator |