Description: Axiom ax-c11 was the original version of ax-c11n ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n could replace it. It appears as Axiom scheme C11' in Megill p. 448 (p. 16 of the preprint).
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11 . (Contributed by NM, 10-May-1993) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-c11 | |- ( A. x x = y -> ( A. x ph -> A. y ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | |- x |
|
| 1 | 0 | cv | |- x |
| 2 | vy | |- y |
|
| 3 | 2 | cv | |- y |
| 4 | 1 3 | wceq | |- x = y |
| 5 | 4 0 | wal | |- A. x x = y |
| 6 | wph | |- ph |
|
| 7 | 6 0 | wal | |- A. x ph |
| 8 | 6 2 | wal | |- A. y ph |
| 9 | 7 8 | wi | |- ( A. x ph -> A. y ph ) |
| 10 | 5 9 | wi | |- ( A. x x = y -> ( A. x ph -> A. y ph ) ) |