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 3533 | . . 3 | |
3 | 1, 2 | uneq12d 3226 | . 2 |
4 | df-suc 4288 | . 2 | |
5 | df-suc 4288 | . 2 | |
6 | 3, 4, 5 | 3eqtr4g 2195 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 cun 3064 csn 3522 csuc 4282 |
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 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-v 2683 df-un 3070 df-sn 3528 df-suc 4288 |
This theorem is referenced by: eqelsuc 4336 2ordpr 4434 onsucsssucexmid 4437 onsucelsucexmid 4440 ordsucunielexmid 4441 suc11g 4467 onsucuni2 4474 0elsucexmid 4475 ordpwsucexmid 4480 peano2 4504 findes 4512 nn0suc 4513 0elnn 4527 omsinds 4530 tfr1onlemsucaccv 6231 tfrcllemsucaccv 6244 tfrcl 6254 frecabcl 6289 frecsuc 6297 sucinc 6334 sucinc2 6335 oacl 6349 oav2 6352 oasuc 6353 oa1suc 6356 nna0r 6367 nnacom 6373 nnaass 6374 nnmsucr 6377 nnsucelsuc 6380 nnsucsssuc 6381 nnaword 6400 nnaordex 6416 phplem3g 6743 nneneq 6744 php5 6745 php5dom 6750 omp1eomlem 6972 omp1eom 6973 indpi 7143 ennnfoneleminc 11913 ennnfonelemex 11916 bj-indsuc 13115 bj-bdfindes 13136 bj-nn0suc0 13137 bj-peano4 13142 bj-inf2vnlem1 13157 bj-nn0sucALT 13165 bj-findes 13168 nnsf 13188 nninfalllemn 13191 nninfsellemdc 13195 nninfself 13198 nninfsellemeqinf 13201 nninfomni 13204 |
Copyright terms: Public domain | W3C validator |