![]() |
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 3948 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ∖ cdif 3795 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-dif 3801 |
This theorem is referenced by: difeq12i 3953 dfin3 4096 indif1 4101 indifcom 4102 difun1 4117 notab 4126 notrab 4133 undifabs 4268 difprsn1 4549 difprsn2 4550 diftpsn3 4551 resdifcom 5652 resdmdfsn 5682 wfi 5953 orddif 6056 fresaun 6312 f12dfv 6784 f13dfv 6785 domunsncan 8329 phplem1 8408 elfiun 8605 axcclem 9594 dfn2 11633 mvdco 18215 pmtrdifellem2 18247 islinds2 20519 lindsind2 20525 restcld 21347 ufprim 22083 volun 23711 itgsplitioo 24003 uhgr0vb 26370 uhgr0 26371 uvtxupgrres 26706 cplgr3v 26733 ex-dif 27838 indifundif 29904 imadifxp 29961 aciunf1 30012 braew 30850 carsgclctunlem1 30924 carsggect 30925 coinflippvt 31092 ballotlemfval0 31103 signstfvcl 31198 frpoind 32279 frind 32282 onint1 32981 bj-2upln1upl 33534 bj-disj2r 33535 lindsenlbs 33948 poimirlem13 33966 poimirlem14 33967 poimirlem18 33971 poimirlem21 33974 poimirlem30 33983 itg2addnclem 34004 asindmre 34038 kelac2 38478 fourierdlem102 41219 fourierdlem114 41231 pwsal 41326 issald 41342 sge0fodjrnlem 41424 hoiprodp1 41596 lincext2 43091 |
Copyright terms: Public domain | W3C validator |