![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > subid1 | Structured version Visualization version GIF version |
Description: Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
subid1 | ⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addrid 11366 | . . 3 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | |
2 | 1 | oveq1d 7399 | . 2 ⊢ (𝐴 ∈ ℂ → ((𝐴 + 0) − 0) = (𝐴 − 0)) |
3 | 0cn 11178 | . . 3 ⊢ 0 ∈ ℂ | |
4 | pncan 11438 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → ((𝐴 + 0) − 0) = 𝐴) | |
5 | 3, 4 | mpan2 689 | . 2 ⊢ (𝐴 ∈ ℂ → ((𝐴 + 0) − 0) = 𝐴) |
6 | 2, 5 | eqtr3d 2773 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2106 (class class class)co 7384 ℂcc 11080 0cc0 11082 + caddc 11085 − cmin 11416 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5283 ax-nul 5290 ax-pow 5347 ax-pr 5411 ax-un 7699 ax-resscn 11139 ax-1cn 11140 ax-icn 11141 ax-addcl 11142 ax-addrcl 11143 ax-mulcl 11144 ax-mulrcl 11145 ax-mulcom 11146 ax-addass 11147 ax-mulass 11148 ax-distr 11149 ax-i2m1 11150 ax-1ne0 11151 ax-1rid 11152 ax-rnegex 11153 ax-rrecex 11154 ax-cnre 11155 ax-pre-lttri 11156 ax-pre-lttrn 11157 ax-pre-ltadd 11158 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3372 df-rab 3426 df-v 3468 df-sbc 3765 df-csb 3881 df-dif 3938 df-un 3940 df-in 3942 df-ss 3952 df-nul 4310 df-if 4514 df-pw 4589 df-sn 4614 df-pr 4616 df-op 4620 df-uni 4893 df-br 5133 df-opab 5195 df-mpt 5216 df-id 5558 df-po 5572 df-so 5573 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-iota 6475 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-riota 7340 df-ov 7387 df-oprab 7388 df-mpo 7389 df-er 8677 df-en 8913 df-dom 8914 df-sdom 8915 df-pnf 11222 df-mnf 11223 df-ltxr 11225 df-sub 11418 |
This theorem is referenced by: subneg 11481 subid1i 11504 subid1d 11532 shftidt2 15000 abs2dif 15251 clim0 15422 rlim0 15424 rlim0lt 15425 climi0 15428 geo2lim 15793 fallfac1 15950 cnbl0 24196 cnblcld 24197 cnfldnm 24201 abelth 25859 logtayl 26074 |
Copyright terms: Public domain | W3C validator |