Description: A variant of ax6 . Axiom scheme C10' 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 axc10 . (Contributed by NM, 10-Jan-1993) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-c10 | |- ( A. x ( x = y -> A. x ph ) -> 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 | wph | |- ph |
|
| 6 | 5 0 | wal | |- A. x ph |
| 7 | 4 6 | wi | |- ( x = y -> A. x ph ) |
| 8 | 7 0 | wal | |- A. x ( x = y -> A. x ph ) |
| 9 | 8 5 | wi | |- ( A. x ( x = y -> A. x ph ) -> ph ) |