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 2188. (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 1822 | . . . 4 wff 𝑧 = 𝑥 |
4 | 3, 1 | wal 1466 | . . 3 wff ∀𝑧 𝑧 = 𝑥 |
5 | 4 | wn 3 | . 2 wff ¬ ∀𝑧 𝑧 = 𝑥 |
6 | vy | . . . . . 6 setvar 𝑦 | |
7 | 1, 6 | weq 1822 | . . . . 5 wff 𝑧 = 𝑦 |
8 | 7, 1 | wal 1466 | . . . 4 wff ∀𝑧 𝑧 = 𝑦 |
9 | 8 | wn 3 | . . 3 wff ¬ ∀𝑧 𝑧 = 𝑦 |
10 | 2, 6 | weq 1822 | . . . 4 wff 𝑥 = 𝑦 |
11 | 10, 1 | wal 1466 | . . . 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: hbae-o 32706 ax13fromc9 32709 equid1 32711 hbequid 32713 equid1ALT 32729 dvelimf-o 32733 ax5eq 32736 |
Copyright terms: Public domain | W3C validator |