Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-c9 | Structured version Visualization version GIF version |
Description: Axiom of Quantifier
Introduction. One of the equality and substitution
axioms of predicate calculus with equality. Informally, it says that
whenever 𝑧 is distinct from 𝑥 and
𝑦,
and 𝑥 =
𝑦 is true,
then 𝑥 = 𝑦 quantified with 𝑧 is also
true. In other words, 𝑧
is irrelevant to the truth of 𝑥 = 𝑦. 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 axc9 2400. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-c9 | ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vz | . . . . 5 setvar 𝑧 | |
2 | vx | . . . . 5 setvar 𝑥 | |
3 | 1, 2 | weq 1964 | . . . 4 wff 𝑧 = 𝑥 |
4 | 3, 1 | wal 1535 | . . 3 wff ∀𝑧 𝑧 = 𝑥 |
5 | 4 | wn 3 | . 2 wff ¬ ∀𝑧 𝑧 = 𝑥 |
6 | vy | . . . . . 6 setvar 𝑦 | |
7 | 1, 6 | weq 1964 | . . . . 5 wff 𝑧 = 𝑦 |
8 | 7, 1 | wal 1535 | . . . 4 wff ∀𝑧 𝑧 = 𝑦 |
9 | 8 | wn 3 | . . 3 wff ¬ ∀𝑧 𝑧 = 𝑦 |
10 | 2, 6 | weq 1964 | . . . 4 wff 𝑥 = 𝑦 |
11 | 10, 1 | wal 1535 | . . . 4 wff ∀𝑧 𝑥 = 𝑦 |
12 | 10, 11 | wi 4 | . . 3 wff (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) |
13 | 9, 12 | wi 4 | . 2 wff (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
14 | 5, 13 | wi 4 | 1 wff (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
Colors of variables: wff setvar class |
This axiom is referenced by: equid1 36050 hbae-o 36054 ax13fromc9 36057 hbequid 36060 equid1ALT 36076 dvelimf-o 36080 ax5eq 36083 |
Copyright terms: Public domain | W3C validator |