Description: Basis step for constructing a substitution instance of ax-c15 without using ax-c15 . We can start with any formula ph in which x is not free. (Contributed by NM, 21-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ax12f.1 | |- ( ph -> A. x ph ) |
|
| Assertion | ax12f | |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax12f.1 | |- ( ph -> A. x ph ) |
|
| 2 | ax-1 | |- ( ph -> ( x = y -> ph ) ) |
|
| 3 | 1 2 | alrimih | |- ( ph -> A. x ( x = y -> ph ) ) |
| 4 | 3 | 2a1i | |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) |