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 2690 | . . . 4 | |
2 | 1 | anbi1d 741 | . . 3 |
3 | elin 3796 | . . 3 | |
4 | elin 3796 | . . 3 | |
5 | 2, 3, 4 | 3bitr4g 303 | . 2 |
6 | 5 | eqrdv 2620 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wceq 1483 wcel 1990 cin 3573 |
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-v 3202 df-in 3581 |
This theorem is referenced by: ineq2 3808 ineq12 3809 ineq1i 3810 ineq1d 3813 unineq 3877 dfrab3ss 3905 intprg 4511 inex1g 4801 reseq1 5390 sspred 5688 isofrlem 6590 qsdisj 7824 fiint 8237 elfiun 8336 dffi3 8337 inf3lema 8521 dfac5lem5 8950 kmlem12 8983 kmlem14 8985 fin23lem24 9144 fin23lem26 9147 fin23lem23 9148 fin23lem22 9149 fin23lem27 9150 ingru 9637 uzin2 14084 incexclem 14568 elrestr 16089 firest 16093 inopn 20704 isbasisg 20751 basis1 20754 basis2 20755 tgval 20759 fctop 20808 cctop 20810 ntrfval 20828 elcls 20877 clsndisj 20879 elcls3 20887 neindisj2 20927 tgrest 20963 restco 20968 restsn 20974 restcld 20976 restcldi 20977 restopnb 20979 neitr 20984 restcls 20985 ordtbaslem 20992 ordtrest2lem 21007 hausnei2 21157 cnhaus 21158 regsep2 21180 dishaus 21186 ordthauslem 21187 cmpsublem 21202 cmpsub 21203 nconnsubb 21226 connsubclo 21227 1stcelcls 21264 islly 21271 cldllycmp 21298 lly1stc 21299 locfincmp 21329 elkgen 21339 ptclsg 21418 dfac14lem 21420 txrest 21434 pthaus 21441 txhaus 21450 xkohaus 21456 xkoptsub 21457 regr1lem 21542 isfbas 21633 fbasssin 21640 fbun 21644 isfil 21651 fbunfip 21673 fgval 21674 filconn 21687 uzrest 21701 isufil2 21712 hauspwpwf1 21791 fclsopni 21819 fclsnei 21823 fclsrest 21828 fcfnei 21839 fcfneii 21841 tsmsfbas 21931 ustincl 22011 ustdiag 22012 ustinvel 22013 ustexhalf 22014 ust0 22023 trust 22033 restutopopn 22042 lpbl 22308 methaus 22325 metrest 22329 restmetu 22375 qtopbaslem 22562 qdensere 22573 xrtgioo 22609 metnrmlem3 22664 icoopnst 22738 iocopnst 22739 ovolicc2lem2 23286 ovolicc2lem5 23289 mblsplit 23300 limcnlp 23642 ellimc3 23643 limcflf 23645 limciun 23658 ig1pval 23932 shincl 28240 shmodi 28249 omlsi 28263 pjoml 28295 chm0 28350 chincl 28358 chdmm1 28384 ledi 28399 cmbr 28443 cmbr3 28467 mdbr 29153 dmdmd 29159 dmdi 29161 dmdbr3 29164 dmdbr4 29165 mdslmd1lem4 29187 cvmd 29195 cvexch 29233 dmdbr6ati 29282 mddmdin0i 29290 difeq 29355 ofpreima2 29466 ordtrest2NEWlem 29968 inelsros 30241 diffiunisros 30242 measvuni 30277 measinb 30284 inelcarsg 30373 carsgclctunlem2 30381 totprob 30489 ballotlemgval 30585 cvmscbv 31240 cvmsdisj 31252 cvmsss2 31256 nepss 31599 brapply 32045 opnbnd 32320 isfne 32334 tailfb 32372 bj-restsn 33035 bj-restpw 33045 bj-rest0 33046 bj-restb 33047 ptrest 33408 poimirlem30 33439 mblfinlem2 33447 bndss 33585 lcvexchlem4 34324 fipjust 37870 ntrkbimka 38336 ntrk0kbimka 38337 clsk3nimkb 38338 isotone2 38347 ntrclskb 38367 ntrclsk3 38368 ntrclsk13 38369 elrestd 39291 islptre 39851 islpcn 39871 subsaliuncllem 40575 subsaliuncl 40576 nnfoctbdjlem 40672 caragensplit 40714 vonvolmbllem 40874 vonvolmbl 40875 incsmflem 40950 decsmflem 40974 smflimlem2 40980 smflimlem3 40981 smflim 40985 smfpimcclem 41013 uzlidlring 41929 rngcvalALTV 41961 rngcval 41962 ringcvalALTV 42007 ringcval 42008 |
Copyright terms: Public domain | W3C validator |