Description: Axiom of Quantifier Introduction. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. Axiom scheme C14' in Megill p. 448 (p. 16 of the preprint). It is redundant if we include ax-5 ; see theorem axc14 . Alternately, ax-5 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 . We retain ax-c14 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 , which might be easier to study for some theoretical purposes.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc14 . (Contributed by NM, 24-Jun-1993) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-c14 | ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑦 → ∀ 𝑧 𝑥 ∈ 𝑦 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vz | ⊢ 𝑧 | |
| 1 | 0 | cv | ⊢ 𝑧 |
| 2 | vx | ⊢ 𝑥 | |
| 3 | 2 | cv | ⊢ 𝑥 |
| 4 | 1 3 | wceq | ⊢ 𝑧 = 𝑥 |
| 5 | 4 0 | wal | ⊢ ∀ 𝑧 𝑧 = 𝑥 |
| 6 | 5 | wn | ⊢ ¬ ∀ 𝑧 𝑧 = 𝑥 |
| 7 | vy | ⊢ 𝑦 | |
| 8 | 7 | cv | ⊢ 𝑦 |
| 9 | 1 8 | wceq | ⊢ 𝑧 = 𝑦 |
| 10 | 9 0 | wal | ⊢ ∀ 𝑧 𝑧 = 𝑦 |
| 11 | 10 | wn | ⊢ ¬ ∀ 𝑧 𝑧 = 𝑦 |
| 12 | 3 8 | wcel | ⊢ 𝑥 ∈ 𝑦 |
| 13 | 12 0 | wal | ⊢ ∀ 𝑧 𝑥 ∈ 𝑦 |
| 14 | 12 13 | wi | ⊢ ( 𝑥 ∈ 𝑦 → ∀ 𝑧 𝑥 ∈ 𝑦 ) |
| 15 | 11 14 | wi | ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑦 → ∀ 𝑧 𝑥 ∈ 𝑦 ) ) |
| 16 | 6 15 | wi | ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑦 → ∀ 𝑧 𝑥 ∈ 𝑦 ) ) ) |