![]() |
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 3040 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dfdif2 3415 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | dfdif2 3415 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3eqtr4g 2512 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-rab 2748 df-dif 3409 |
This theorem is referenced by: difeq12 3548 difeq1i 3549 difeq1d 3552 symdifeq1 3667 uneqdifeq 3858 hartogslem1 8062 kmlem9 8593 kmlem11 8595 kmlem12 8596 isfin1a 8727 fin1a2lem13 8847 incexclem 13906 coprmprod 14690 coprmproddvds 14692 ismri 15549 f1otrspeq 17100 pmtrval 17104 pmtrfrn 17111 symgsssg 17120 symgfisg 17121 symggen 17123 psgnunilem1 17146 psgnunilem5 17147 psgneldm 17156 ablfac1eulem 17717 islbs 18311 lbsextlem1 18393 lbsextlem2 18394 lbsextlem3 18395 lbsextlem4 18396 zrhcofipsgn 19173 submafval 19616 m1detdiag 19634 lpval 20167 2ndcdisj 20483 isufil 20930 ptcmplem2 21080 mblsplit 22498 voliunlem3 22517 ig1pval 23136 ig1pvalOLD 23142 nb3graprlem2 25192 iscusgra 25196 isuvtx 25228 isfrgra 25730 1vwmgra 25743 3vfriswmgra 25745 difeq 28163 sigaval 28944 issiga 28945 issgon 28957 isros 29002 unelros 29005 difelros 29006 inelsros 29012 diffiunisros 29013 rossros 29014 inelcarsg 29155 carsgclctunlem2 29163 probun 29264 ballotlemgval 29368 ballotlemgvalOLD 29406 cvmscbv 29993 cvmsi 30000 cvmsval 30001 poimirlem4 31956 sdrgacs 36079 compne 36804 dvmptfprod 37830 caragensplit 38331 nbgr2vtx1edg 39428 nbuhgr2vtx1edgb 39430 nbgr0vtx 39434 nb3grprlem2 39465 uvtxa01vtx0 39479 cplgr1v 39507 ldepsnlinc 40405 |
Copyright terms: Public domain | W3C validator |