Description: Derive set.mm's original ax-c9 from the shorter ax-13 . Usage is discouraged to avoid uninformed ax-13 propagation. (Contributed by NM, 29-Nov-2015) (Revised by NM, 24-Dec-2015) (Proof shortened by Wolf Lammen, 29-Apr-2018) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axc9 | |- ( -. A. z z = x -> ( -. A. z z = y -> ( x = y -> A. z x = y ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfeqf | |- ( ( -. A. z z = x /\ -. A. z z = y ) -> F/ z x = y ) |
|
| 2 | 1 | nf5rd | |- ( ( -. A. z z = x /\ -. A. z z = y ) -> ( x = y -> A. z x = y ) ) |
| 3 | 2 | ex | |- ( -. A. z z = x -> ( -. A. z z = y -> ( x = y -> A. z x = y ) ) ) |