| 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 2387. (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 1962 | . . . 4 wff 𝑧 = 𝑥 |
| 4 | 3, 1 | wal 1538 | . . 3 wff ∀𝑧 𝑧 = 𝑥 |
| 5 | 4 | wn 3 | . 2 wff ¬ ∀𝑧 𝑧 = 𝑥 |
| 6 | vy | . . . . . 6 setvar 𝑦 | |
| 7 | 1, 6 | weq 1962 | . . . . 5 wff 𝑧 = 𝑦 |
| 8 | 7, 1 | wal 1538 | . . . 4 wff ∀𝑧 𝑧 = 𝑦 |
| 9 | 8 | wn 3 | . . 3 wff ¬ ∀𝑧 𝑧 = 𝑦 |
| 10 | 2, 6 | weq 1962 | . . . 4 wff 𝑥 = 𝑦 |
| 11 | 10, 1 | wal 1538 | . . . 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 38900 hbae-o 38904 ax13fromc9 38907 hbequid 38910 equid1ALT 38926 dvelimf-o 38930 ax5eq 38933 |
| Copyright terms: Public domain | W3C validator |