![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > difeq2 | 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 |
---|---|
difeq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2529 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | notbid 300 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rabbidv 3048 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | dfdif2 3425 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | dfdif2 3425 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3eqtr4g 2521 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-ral 2754 df-rab 2758 df-dif 3419 |
This theorem is referenced by: difeq12 3558 difeq2i 3560 difeq2d 3563 symdifeq1 3677 disjdif2 3858 ssdifeq0 3862 sorpsscmpl 6609 2oconcl 7231 oev 7242 sbthlem2 7709 sbth 7718 infdiffi 8189 fin1ai 8749 fin23lem7 8772 fin23lem11 8773 compsscnv 8827 isf34lem1 8828 compss 8832 isf34lem4 8833 fin1a2lem7 8862 pwfseqlem4a 9112 pwfseqlem4 9113 efgmval 17411 efgi 17418 frgpuptinv 17470 gsumcllem 17591 gsumzaddlem 17603 fctop 20068 cctop 20070 iscld 20091 clsval2 20114 opncldf1 20149 opncldf2 20150 opncldf3 20151 indiscld 20156 mretopd 20157 restcld 20237 lecldbas 20284 pnrmopn 20408 hauscmplem 20470 elpt 20636 elptr 20637 cfinfil 20957 csdfil 20958 ufilss 20969 filufint 20984 cfinufil 20992 ufinffr 20993 ufilen 20994 prdsxmslem2 21593 lebnumlem1 22038 lebnumlem1OLD 22041 bcth3 22348 ismbl 22529 ishpg 24850 frgrawopreg1 25827 frgrawopreg2 25828 disjdifprg 28234 0elsiga 28985 prsiga 29002 sigaclci 29003 difelsiga 29004 unelldsys 29029 sigapildsyslem 29032 sigapildsys 29033 ldgenpisyslem1 29034 isros 29039 unelros 29042 difelros 29043 inelsros 29049 diffiunisros 29050 rossros 29051 elcarsg 29186 ballotlemfval 29371 ballotlemgval 29405 ballotlemgvalOLD 29443 kur14lem1 29978 topdifinffinlem 31795 topdifinffin 31796 prsal 38217 saldifcl 38218 salexct 38231 salexct2 38236 salexct3 38239 salgencntex 38240 salgensscntex 38241 caragenel 38354 |
Copyright terms: Public domain | W3C validator |