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 | |- ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vz | |- z |
|
| 1 | 0 | cv | |- z |
| 2 | vx | |- x |
|
| 3 | 2 | cv | |- x |
| 4 | 1 3 | wceq | |- z = x |
| 5 | 4 0 | wal | |- A. z z = x |
| 6 | 5 | wn | |- -. A. z z = x |
| 7 | vy | |- y |
|
| 8 | 7 | cv | |- y |
| 9 | 1 8 | wceq | |- z = y |
| 10 | 9 0 | wal | |- A. z z = y |
| 11 | 10 | wn | |- -. A. z z = y |
| 12 | 3 8 | wcel | |- x e. y |
| 13 | 12 0 | wal | |- A. z x e. y |
| 14 | 12 13 | wi | |- ( x e. y -> A. z x e. y ) |
| 15 | 11 14 | wi | |- ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) |
| 16 | 6 15 | wi | |- ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) ) |