![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > difeq2i | Structured version Visualization version GIF version |
Description: Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
Ref | Expression |
---|---|
difeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
difeq2i | ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | difeq2 3985 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1508 ∖ cdif 3828 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2752 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2761 df-cleq 2773 df-clel 2848 df-ral 3095 df-rab 3099 df-dif 3834 |
This theorem is referenced by: difeq12i 3989 dfun3 4132 dfin3 4133 dfin4 4134 invdif 4135 indif 4136 difundi 4146 difindi 4148 difdif2 4151 dif32 4157 difabs 4158 dfsymdif3 4159 notrab 4170 dif0 4221 unvdif 4309 difdifdir 4323 dfif3 4367 difpr 4615 iinvdif 4873 cnvin 5848 fndifnfp 6767 dif1o 7933 dfsdom2 8442 dju1dif 9402 m1bits 15655 clsval2 21377 mretopd 21419 cmpfi 21735 llycmpkgen2 21877 pserdvlem2 24734 nbgrssvwo2 26862 finsumvtxdg2ssteplem1 27045 frgrwopreglem3 27863 iundifdifd 30099 iundifdif 30100 difres 30133 sibfof 31275 eulerpartlemmf 31310 kur14lem2 32079 kur14lem6 32083 kur14lem7 32084 dfon4 32915 onint1 33357 bj-2upln1upl 33894 poimirlem8 34381 dfssr2 35224 prjspval2 38711 diophren 38847 nonrel 39347 dssmapntrcls 39882 salincl 42074 meaiuninc 42229 carageniuncllem1 42269 |
Copyright terms: Public domain | W3C validator |