Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > difeq2i | Structured version Visualization version Unicode version |
Description: Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
Ref | Expression |
---|---|
difeq1i.1 |
Ref | Expression |
---|---|
difeq2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difeq1i.1 | . 2 | |
2 | difeq2 3722 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1483 cdif 3571 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-ral 2917 df-rab 2921 df-dif 3577 |
This theorem is referenced by: difeq12i 3726 dfun3 3865 dfin3 3866 dfin4 3867 invdif 3868 indif 3869 difundi 3879 difindi 3881 difdif2 3884 dif32 3891 difabs 3892 dfsymdif3 3893 notrab 3904 dif0 3950 unvdif 4042 difdifdir 4056 dfif3 4100 difpr 4334 iinvdif 4592 cnvin 5540 fndifnfp 6442 dif1o 7580 dfsdom2 8083 cda1dif 8998 m1bits 15162 clsval2 20854 mretopd 20896 cmpfi 21211 llycmpkgen2 21353 pserdvlem2 24182 nbgrssvwo2 26261 finsumvtxdg2ssteplem1 26441 clwwlknclwwlkdifs 26873 frgrwopreglem3 27178 iundifdifd 29380 iundifdif 29381 difres 29413 sibfof 30402 eulerpartlemmf 30437 kur14lem2 31189 kur14lem6 31193 kur14lem7 31194 dfon4 32000 onint1 32448 bj-2upln1upl 33012 poimirlem8 33417 diophren 37377 nonrel 37890 dssmapntrcls 38426 salincl 40543 meaiuninc 40698 carageniuncllem1 40735 |
Copyright terms: Public domain | W3C validator |