Description: This theorem shows that Axiom ax-c16 is redundant in the presence of Theorem dtru , which states simply that at least two things exist. This justifies the remark at mmzfcnd.html#twoness (which links to this theorem). (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 7-Nov-2006)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axc16b | |- ( A. x x = y -> ( ph -> A. x ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dtru | |- -. A. x x = y |
|
| 2 | 1 | pm2.21i | |- ( A. x x = y -> ( ph -> A. x ph ) ) |