Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > suceq | Unicode version |
Description: Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
suceq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . . 3 | |
2 | sneq 3538 | . . 3 | |
3 | 1, 2 | uneq12d 3231 | . 2 |
4 | df-suc 4293 | . 2 | |
5 | df-suc 4293 | . 2 | |
6 | 3, 4, 5 | 3eqtr4g 2197 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 cun 3069 csn 3527 csuc 4287 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-un 3075 df-sn 3533 df-suc 4293 |
This theorem is referenced by: eqelsuc 4341 2ordpr 4439 onsucsssucexmid 4442 onsucelsucexmid 4445 ordsucunielexmid 4446 suc11g 4472 onsucuni2 4479 0elsucexmid 4480 ordpwsucexmid 4485 peano2 4509 findes 4517 nn0suc 4518 0elnn 4532 omsinds 4535 tfr1onlemsucaccv 6238 tfrcllemsucaccv 6251 tfrcl 6261 frecabcl 6296 frecsuc 6304 sucinc 6341 sucinc2 6342 oacl 6356 oav2 6359 oasuc 6360 oa1suc 6363 nna0r 6374 nnacom 6380 nnaass 6381 nnmsucr 6384 nnsucelsuc 6387 nnsucsssuc 6388 nnaword 6407 nnaordex 6423 phplem3g 6750 nneneq 6751 php5 6752 php5dom 6757 omp1eomlem 6979 omp1eom 6980 indpi 7150 ennnfoneleminc 11924 ennnfonelemex 11927 bj-indsuc 13126 bj-bdfindes 13147 bj-nn0suc0 13148 bj-peano4 13153 bj-inf2vnlem1 13168 bj-nn0sucALT 13176 bj-findes 13179 nnsf 13199 nninfalllemn 13202 nninfsellemdc 13206 nninfself 13209 nninfsellemeqinf 13212 nninfomni 13215 |
Copyright terms: Public domain | W3C validator |