![]() |
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 11373 | . . 3 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | |
2 | 1 | oveq1d 7405 | . 2 ⊢ (𝐴 ∈ ℂ → ((𝐴 + 0) − 0) = (𝐴 − 0)) |
3 | 0cn 11185 | . . 3 ⊢ 0 ∈ ℂ | |
4 | pncan 11445 | . . 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 7390 ℂcc 11087 0cc0 11089 + caddc 11092 − cmin 11423 |
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 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7705 ax-resscn 11146 ax-1cn 11147 ax-icn 11148 ax-addcl 11149 ax-addrcl 11150 ax-mulcl 11151 ax-mulrcl 11152 ax-mulcom 11153 ax-addass 11154 ax-mulass 11155 ax-distr 11156 ax-i2m1 11157 ax-1ne0 11158 ax-1rid 11159 ax-rnegex 11160 ax-rrecex 11161 ax-cnre 11162 ax-pre-lttri 11163 ax-pre-lttrn 11164 ax-pre-ltadd 11165 |
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 3376 df-rab 3430 df-v 3472 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4520 df-pw 4595 df-sn 4620 df-pr 4622 df-op 4626 df-uni 4899 df-br 5139 df-opab 5201 df-mpt 5222 df-id 5564 df-po 5578 df-so 5579 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6481 df-fun 6531 df-fn 6532 df-f 6533 df-f1 6534 df-fo 6535 df-f1o 6536 df-fv 6537 df-riota 7346 df-ov 7393 df-oprab 7394 df-mpo 7395 df-er 8683 df-en 8920 df-dom 8921 df-sdom 8922 df-pnf 11229 df-mnf 11230 df-ltxr 11232 df-sub 11425 |
This theorem is referenced by: subneg 11488 subid1i 11511 subid1d 11539 shftidt2 15007 abs2dif 15258 clim0 15429 rlim0 15431 rlim0lt 15432 climi0 15435 geo2lim 15800 fallfac1 15957 cnbl0 24214 cnblcld 24215 cnfldnm 24219 abelth 25877 logtayl 26092 |
Copyright terms: Public domain | W3C validator |