![]() |
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 4115 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∖ cdif 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-dif 3950 |
This theorem is referenced by: difeq12i 4119 dfun3 4267 dfin3 4268 dfin4 4269 invdif 4270 indif 4271 difundi 4281 difindi 4283 difdif2 4288 dif32 4294 difabs 4295 dfsymdif3 4298 notrab 4314 dif0 4377 unvdif 4479 difdifdir 4496 dfif3 4547 difpr 4812 iinvdif 5088 cnvin 6156 fndifnfp 7190 dif1o 8530 dfsdom2 9134 brttrcl2 9757 ttrcltr 9759 rnttrcl 9765 dju1dif 10215 m1bits 16440 clsval2 23045 mretopd 23087 cmpfi 23403 llycmpkgen2 23545 pserdvlem2 26458 nbgrssvwo2 29298 finsumvtxdg2ssteplem1 29482 frgrwopreglem3 30247 iundifdifd 32482 iundifdif 32483 difres 32520 gsumhashmul 32925 pmtrcnelor 32969 cycpmconjv 33020 cyc3conja 33035 sibfof 34174 eulerpartlemmf 34209 kur14lem2 35035 kur14lem6 35039 kur14lem7 35040 satfv1 35191 dfon4 35717 onint1 36161 bj-2upln1upl 36731 poimirlem8 37329 dfssr2 38197 prjspval2 42267 diophren 42470 ordeldif1o 42926 nonrel 43251 dssmapntrcls 43795 salincl 45945 meaiuninc 46102 carageniuncllem1 46142 iscnrm3rlem3 48276 |
Copyright terms: Public domain | W3C validator |