| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > difeq1i | Structured version Visualization version GIF version | ||
| Description: Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.) |
| Ref | Expression |
|---|---|
| difeq1i.1 | ⊢ 𝐴 = 𝐵 |
| Ref | Expression |
|---|---|
| difeq1i | ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | difeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 2 | difeq1 4119 | . 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 dfin3 4277 indif1 4282 indifcom 4283 difun1 4299 notab 4314 rabdif 4321 notrab 4322 undifabs 4478 difprsn1 4800 difprsn2 4801 diftpsn3 4802 resdifcom 6016 resdmdfsn 6049 frpoind 6363 wfiOLD 6372 orddif 6480 fresaun 6779 f12dfv 7293 f13dfv 7294 domunsncan 9112 phplem1OLD 9254 elfiun 9470 frind 9790 dju1dif 10213 axcclem 10497 dfn2 12539 mvdco 19463 pmtrdifellem2 19495 islinds2 21833 lindsind2 21839 restcld 23180 ufprim 23917 volun 25580 itgsplitioo 25873 uhgr0vb 29089 uhgr0 29090 uvtxupgrres 29425 cplgr3v 29452 ex-dif 30442 indifundif 32543 imadifxp 32614 aciunf1 32673 indsupp 32852 s1chn 33000 pmtrcnelor 33111 lindsunlem 33675 lindsun 33676 braew 34243 carsgclctunlem1 34319 carsggect 34320 coinflippvt 34487 ballotlemfval0 34498 signstfvcl 34588 satf0 35377 onint1 36450 bj-2upln1upl 37025 bj-disj2r 37029 lindsenlbs 37622 poimirlem13 37640 poimirlem14 37641 poimirlem18 37645 poimirlem21 37648 poimirlem30 37657 itg2addnclem 37678 asindmre 37710 sucdifsn 38240 disjresundif 38244 ressucdifsn 38246 kelac2 43077 fourierdlem102 46223 fourierdlem114 46235 pwsal 46330 issald 46348 sge0fodjrnlem 46431 hoiprodp1 46603 lincext2 48372 disjdifb 48729 |
| Copyright terms: Public domain | W3C validator |