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 36037 hbae-o 36041 ax13fromc9 36044 hbequid 36047 equid1ALT 36063 dvelimf-o 36067 ax5eq 36070 |
Copyright terms: Public domain | W3C validator |