![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ineq1 | Structured version Visualization version Unicode version |
Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) |
Ref | Expression |
---|---|
ineq1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2528 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anbi1d 716 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | elin 3628 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | elin 3628 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3bitr4g 296 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | eqrdv 2459 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-v 3058 df-in 3422 |
This theorem is referenced by: ineq2 3639 ineq12 3640 ineq1i 3641 ineq1d 3644 unineq 3704 dfrab3ss 3732 intprg 4282 inex1g 4559 reseq1 5117 sspred 5406 isofrlem 6255 qsdisj 7465 fiint 7873 elfiun 7969 dffi3 7970 inf3lema 8154 dfac5lem5 8583 kmlem12 8616 kmlem14 8618 fin23lem24 8777 fin23lem26 8780 fin23lem23 8781 fin23lem22 8782 fin23lem27 8783 ingru 9265 uzin2 13455 incexclem 13942 elrestr 15375 firest 15379 inopn 19977 isbasisg 20010 basis1 20013 basis2 20014 tgval 20018 fctop 20067 cctop 20069 ntrfval 20087 elcls 20137 clsndisj 20139 elcls3 20147 neindisj2 20187 tgrest 20223 restco 20228 restsn 20234 restcld 20236 restcldi 20237 restopnb 20239 neitr 20244 restcls 20245 ordtbaslem 20252 ordtrest2lem 20267 hausnei2 20417 cnhaus 20418 regsep2 20440 dishaus 20446 ordthauslem 20447 cmpsublem 20462 cmpsub 20463 nconsubb 20486 consubclo 20487 1stcelcls 20524 islly 20531 cldllycmp 20558 lly1stc 20559 locfincmp 20589 elkgen 20599 ptclsg 20678 dfac14lem 20680 txrest 20694 pthaus 20701 txhaus 20710 xkohaus 20716 xkoptsub 20717 regr1lem 20802 isfbas 20892 fbasssin 20899 fbun 20903 isfil 20910 fbunfip 20932 fgval 20933 filcon 20946 uzrest 20960 isufil2 20971 hauspwpwf1 21050 fclsopni 21078 fclsnei 21082 fclsrest 21087 fcfnei 21098 fcfneii 21100 tsmsfbas 21190 ustincl 21270 ustdiag 21271 ustinvel 21272 ustexhalf 21273 ust0 21282 trust 21292 restutopopn 21301 lpbl 21566 methaus 21583 metrest 21587 restmetu 21633 qtopbaslem 21827 qdensere 21838 xrtgioo 21872 metnrmlem3 21926 metnrmlem3OLD 21941 icoopnst 22015 iocopnst 22016 ovolicc2lem2 22519 ovolicc2lem5 22523 mblsplit 22534 limcnlp 22881 ellimc3 22882 limcflf 22884 limciun 22897 ig1pval 23172 ig1pvalOLD 23178 shincl 27082 shmodi 27091 omlsi 27105 pjoml 27137 chm0 27192 chincl 27200 chdmm1 27226 ledi 27241 cmbr 27285 cmbr3 27309 mdbr 27995 dmdmd 28001 dmdi 28003 dmdbr3 28006 dmdbr4 28007 mdslmd1lem4 28029 cvmd 28037 cvexch 28075 dmdbr6ati 28124 mddmdin0i 28132 difeq 28199 ofpreima2 28317 ordtrest2NEWlem 28776 inelsros 29048 diffiunisros 29049 measvuni 29084 measinb 29091 inelcarsg 29191 carsgclctunlem2 29199 totprob 29308 ballotlemgval 29404 ballotlemgvalOLD 29442 cvmscbv 30029 cvmsdisj 30041 cvmsss2 30045 nepss 30398 brapply 30753 opnbnd 31029 isfne 31043 tailfb 31081 ptrest 31983 poimirlem30 32014 mblfinlem2 32022 bndss 32162 lcvexchlem4 32647 fipjust 36213 islptre 37736 islpcn 37756 nnfoctbdjlem 38330 caragensplit 38358 uzlidlring 40201 rngcvalALTV 40235 rngcval 40236 ringcvalALTV 40281 ringcval 40282 |
Copyright terms: Public domain | W3C validator |