| 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 4120 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∖ cdif 3948 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-dif 3954 |
| This theorem is referenced by: difeq12i 4124 dfun3 4276 dfin3 4277 dfin4 4278 invdif 4279 indif 4280 difundi 4290 difindi 4292 difdif2 4296 dif32 4302 difabs 4303 dfsymdif3 4306 notrab 4322 dif0 4378 unvdif 4475 difdifdir 4492 dfif3 4540 difpr 4803 iinvdif 5080 cnvin 6164 fndifnfp 7196 dif1o 8538 dfsdom2 9136 brttrcl2 9754 ttrcltr 9756 rnttrcl 9762 dju1dif 10213 m1bits 16477 clsval2 23058 mretopd 23100 cmpfi 23416 llycmpkgen2 23558 pserdvlem2 26472 nbgrssvwo2 29379 finsumvtxdg2ssteplem1 29563 frgrwopreglem3 30333 iundifdifd 32574 iundifdif 32575 difres 32613 gsumhashmul 33064 pmtrcnelor 33111 cycpmconjv 33162 cyc3conja 33177 elrgspnsubrunlem2 33252 sibfof 34342 eulerpartlemmf 34377 kur14lem2 35212 kur14lem6 35216 kur14lem7 35217 satfv1 35368 dfon4 35894 onint1 36450 bj-2upln1upl 37025 poimirlem8 37635 dfssr2 38500 prjspval2 42623 diophren 42824 ordeldif1o 43273 nonrel 43597 dssmapntrcls 44141 salincl 46339 meaiuninc 46496 carageniuncllem1 46536 iscnrm3rlem3 48839 |
| Copyright terms: Public domain | W3C validator |