Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nnasuc | Structured version Visualization version GIF version |
Description: Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
Ref | Expression |
---|---|
nnasuc | ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnon 7608 | . 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On) | |
2 | onasuc 8187 | . 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) | |
3 | 1, 2 | sylan 583 | 1 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1542 ∈ wcel 2114 Oncon0 6173 suc csuc 6175 (class class class)co 7173 ωcom 7602 +o coa 8131 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-sep 5168 ax-nul 5175 ax-pr 5297 ax-un 7482 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3401 df-sbc 3682 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-iun 4884 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-ov 7176 df-oprab 7177 df-mpo 7178 df-om 7603 df-wrecs 7979 df-recs 8040 df-rdg 8078 df-oadd 8138 |
This theorem is referenced by: nna0r 8269 nnacl 8271 nnacom 8277 nnaordi 8278 nnawordi 8281 nnaass 8282 nndi 8283 nnmsucr 8285 nnawordex 8297 nneob 8313 omopthlem1 8316 nnadju 9700 ackbij1lem14 9736 ackbij1lem18 9740 hashgadd 13833 finxpreclem4 35211 |
Copyright terms: Public domain | W3C validator |