| 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 4074 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: = wceq 1570 ∖ cdif 3903 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2737 |
| This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-sb 2100 df-clab 2744 df-cleq 2757 df-clel 2840 df-rab 3419 df-dif 3909 |
| This theorem is used by: difeq12i 4079 dfin3 4230 indif1 4235 indifcom 4236 difun1 4252 notab 4267 rabdif 4274 notrab 4275 undifabs 4441 difprsn1 4770 difprsn2 4771 diftpsn3 4772 resdifcom 5999 resdmdfsn 6033 resdmdfsnOLD 6034 frpoind 6347 orddif 6463 fresaun 6753 f12dfv 7280 f13dfv 7281 domunsncan 9072 elfiun 9397 frind 9729 dju1dif 10172 axcclem 10456 dfn2 12532 nulchn 18697 s1chn 18698 chnccat 18704 ex-chn1 18715 ex-chn2 18716 mvdco 19559 pmtrdifellem2 19591 islinds2 22013 lindsind2 22019 restcld 23379 ufprim 24117 volun 25755 itgsplitioo 26048 uhgr0vb 29477 uhgr0 29478 uvtxupgrres 29816 cplgr3v 29843 ex-dif 30845 indifundif 32941 imadifxp 33017 aciunf1 33079 indsupp 33257 pmtrcnelor 33475 lindsunlem 34078 lindsun 34079 braew 34697 carsgclctunlem1 34772 carsggect 34773 coinflippvt 34940 ballotlemfval0 34951 signstfvcl 35025 satf0 35901 onint1 37017 bj-2upln1upl 37717 bj-disj2r 37721 lindsenlbs 38323 poimirlem13 38341 poimirlem14 38342 poimirlem18 38346 poimirlem21 38349 poimirlem30 38358 itg2addnclem 38379 asindmre 38411 disjresundif 38953 dmxrnuncnvepres 39099 dmxrncnvepres2 39140 sucdifsn 39193 ressucdifsn 39195 kelac2 43850 fourierdlem102 46980 fourierdlem114 46992 pwsal 47087 issald 47105 sge0fodjrnlem 47188 hoiprodp1 47360 lincext2 49292 disjdifb 49645 |
| Copyright terms: Public domain | W3C validator |