![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > difeq1i | Structured version Visualization version Unicode 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 3544 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-rab 2746 df-dif 3407 |
This theorem is referenced by: difeq12i 3549 dfin3 3682 indif1 3687 indifcom 3688 difun1 3703 notab 3713 notrab 3720 undifabs 3844 difprsn1 4108 difprsn2 4109 resdmdfsn 5150 wfi 5413 orddif 5516 fresaun 5754 f12dfv 6172 f13dfv 6173 domunsncan 7672 phplem1 7751 elfiun 7944 axcclem 8887 dfn2 10882 mvdco 17086 pmtrdifellem2 17118 islinds2 19371 lindsind2 19377 restcld 20188 ufprim 20924 volun 22498 itgsplitioo 22795 uhgra0v 25037 usgra0v 25098 usgra1v 25117 cusgra3v 25192 ex-dif 25873 indifundif 28152 imadifxp 28212 aciunf1 28265 braew 29065 carsgclctunlem1 29149 carsggect 29150 coinflippvt 29317 ballotlemfval0 29328 signstfvcl 29462 frind 30481 onint1 31109 bj-2upln1upl 31618 poimirlem13 31953 poimirlem14 31954 poimirlem18 31958 poimirlem21 31961 poimirlem30 31970 itg2addnclem 31993 asindmre 32027 kelac2 35923 fourierdlem102 38072 fourierdlem114 38084 pwsal 38176 issald 38192 sge0fodjrnlem 38258 hoiprodp1 38410 uhgr0vb 39165 uhgr0 39166 usgr1vr 39329 uvtxupgrres 39481 cplgr3v 39502 uhg0v 39742 uhgrepe 39743 lincext2 40301 |
Copyright terms: Public domain | W3C validator |