![]() |
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 4111 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∖ cdif 3941 |
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 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-rab 3428 df-dif 3947 |
This theorem is referenced by: difeq12i 4116 dfin3 4262 indif1 4267 indifcom 4268 difun1 4285 notab 4300 notrab 4307 undifabs 4473 difprsn1 4799 difprsn2 4800 diftpsn3 4801 resdifcom 5998 resdmdfsn 6029 frpoind 6342 wfiOLD 6351 orddif 6459 fresaun 6762 f12dfv 7276 f13dfv 7277 domunsncan 9090 phplem1OLD 9235 elfiun 9447 frind 9767 dju1dif 10189 axcclem 10474 dfn2 12509 mvdco 19393 pmtrdifellem2 19425 islinds2 21740 lindsind2 21746 restcld 23069 ufprim 23806 volun 25467 itgsplitioo 25760 uhgr0vb 28878 uhgr0 28879 uvtxupgrres 29214 cplgr3v 29241 ex-dif 30226 indifundif 32314 imadifxp 32384 aciunf1 32442 pmtrcnelor 32808 lindsunlem 33308 lindsun 33309 braew 33851 carsgclctunlem1 33927 carsggect 33928 coinflippvt 34094 ballotlemfval0 34105 signstfvcl 34195 satf0 34972 onint1 35923 bj-2upln1upl 36493 bj-disj2r 36497 lindsenlbs 37077 poimirlem13 37095 poimirlem14 37096 poimirlem18 37100 poimirlem21 37103 poimirlem30 37112 itg2addnclem 37133 asindmre 37165 sucdifsn 37698 disjresundif 37702 ressucdifsn 37704 rabdif 41675 kelac2 42461 fourierdlem102 45568 fourierdlem114 45580 pwsal 45675 issald 45693 sge0fodjrnlem 45776 hoiprodp1 45948 lincext2 47495 disjdifb 47852 |
Copyright terms: Public domain | W3C validator |