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 2338. (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 1931 | . . . 4 wff 𝑧 = 𝑥 |
4 | 3, 1 | wal 1521 | . . 3 wff ∀𝑧 𝑧 = 𝑥 |
5 | 4 | wn 3 | . 2 wff ¬ ∀𝑧 𝑧 = 𝑥 |
6 | vy | . . . . . 6 setvar 𝑦 | |
7 | 1, 6 | weq 1931 | . . . . 5 wff 𝑧 = 𝑦 |
8 | 7, 1 | wal 1521 | . . . 4 wff ∀𝑧 𝑧 = 𝑦 |
9 | 8 | wn 3 | . . 3 wff ¬ ∀𝑧 𝑧 = 𝑦 |
10 | 2, 6 | weq 1931 | . . . 4 wff 𝑥 = 𝑦 |
11 | 10, 1 | wal 1521 | . . . 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 34503 hbae-o 34507 ax13fromc9 34510 hbequid 34513 equid1ALT 34529 dvelimf-o 34533 ax5eq 34536 |
Copyright terms: Public domain | W3C validator |