Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > difeq1 | Structured version Visualization version Unicode version |
Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
difeq1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabeq 3192 | . 2 | |
2 | dfdif2 3583 | . 2 | |
3 | dfdif2 3583 | . 2 | |
4 | 1, 2, 3 | 3eqtr4g 2681 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wceq 1483 wcel 1990 crab 2916 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-nfc 2753 df-rab 2921 df-dif 3577 |
This theorem is referenced by: difeq12 3723 difeq1i 3724 difeq1d 3727 symdifeq1 3846 uneqdifeq 4057 uneqdifeqOLD 4058 hartogslem1 8447 kmlem9 8980 kmlem11 8982 kmlem12 8983 isfin1a 9114 fin1a2lem13 9234 fundmge2nop0 13274 incexclem 14568 coprmprod 15375 coprmproddvds 15377 ismri 16291 f1otrspeq 17867 pmtrval 17871 pmtrfrn 17878 symgsssg 17887 symgfisg 17888 symggen 17890 psgnunilem1 17913 psgnunilem5 17914 psgneldm 17923 ablfac1eulem 18471 islbs 19076 lbsextlem1 19158 lbsextlem2 19159 lbsextlem3 19160 lbsextlem4 19161 zrhcofipsgn 19939 submafval 20385 m1detdiag 20403 lpval 20943 2ndcdisj 21259 isufil 21707 ptcmplem2 21857 mblsplit 23300 voliunlem3 23320 ig1pval 23932 nbgr2vtx1edg 26246 nbuhgr2vtx1edgb 26248 nbgr0vtx 26252 nb3grprlem2 26283 uvtxa01vtx0 26297 cplgr1v 26326 dfconngr1 27048 isconngr1 27050 isfrgr 27122 frgr1v 27135 nfrgr2v 27136 frgr3v 27139 1vwmgr 27140 3vfriswmgr 27142 difeq 29355 sigaval 30173 issiga 30174 issgon 30186 isros 30231 unelros 30234 difelros 30235 inelsros 30241 diffiunisros 30242 rossros 30243 inelcarsg 30373 carsgclctunlem2 30381 probun 30481 ballotlemgval 30585 cvmscbv 31240 cvmsi 31247 cvmsval 31248 poimirlem4 33413 sdrgacs 37771 dssmapfvd 38311 compne 38643 compneOLD 38644 dvmptfprod 40160 caragensplit 40714 vonvolmbllem 40874 vonvolmbl 40875 ldepsnlinc 42297 |
Copyright terms: Public domain | W3C validator |