Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > intss1 | Structured version Visualization version Unicode version |
Description: An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995.) |
Ref | Expression |
---|---|
intss1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3203 | . . . 4 | |
2 | 1 | elint 4481 | . . 3 |
3 | eleq1 2689 | . . . . . 6 | |
4 | eleq2 2690 | . . . . . 6 | |
5 | 3, 4 | imbi12d 334 | . . . . 5 |
6 | 5 | spcgv 3293 | . . . 4 |
7 | 6 | pm2.43a 54 | . . 3 |
8 | 2, 7 | syl5bi 232 | . 2 |
9 | 8 | ssrdv 3609 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wal 1481 wceq 1483 wcel 1990 wss 3574 cint 4475 |
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 df-ss 3588 df-int 4476 |
This theorem is referenced by: intminss 4503 intmin3 4505 intab 4507 int0el 4508 trintss 4769 intex 4820 oneqmini 5776 sorpssint 6947 onint 6995 onssmin 6997 onnmin 7003 nnawordex 7717 dffi2 8329 inficl 8331 dffi3 8337 tcmin 8617 tc2 8618 rankr1ai 8661 rankuni2b 8716 tcrank 8747 harval2 8823 cfflb 9081 fin23lem20 9159 fin23lem38 9171 isf32lem2 9176 intwun 9557 inttsk 9596 intgru 9636 dfnn2 11033 dfuzi 11468 trclubi 13735 trclubiOLD 13736 trclubgi 13737 trclubgiOLD 13738 trclub 13739 trclubg 13740 cotrtrclfv 13753 trclun 13755 dfrtrcl2 13802 mremre 16264 isacs1i 16318 mrelatglb 17184 cycsubg 17622 efgrelexlemb 18163 efgcpbllemb 18168 frgpuplem 18185 cssmre 20037 toponmre 20897 1stcfb 21248 ptcnplem 21424 fbssfi 21641 uffix 21725 ufildom1 21730 alexsublem 21848 alexsubALTlem4 21854 tmdgsum2 21900 bcth3 23128 limciun 23658 aalioulem3 24089 shintcli 28188 shsval2i 28246 ococin 28267 chsupsn 28272 insiga 30200 ldsysgenld 30223 ldgenpisyslem2 30227 mclsssvlem 31459 mclsax 31466 mclsind 31467 untint 31589 dfon2lem8 31695 dfon2lem9 31696 sltval2 31809 sltres 31815 nocvxminlem 31893 scutun12 31917 scutbdaybnd 31921 scutbdaylt 31922 clsint2 32324 topmeet 32359 topjoin 32360 heibor1lem 33608 ismrcd1 37261 mzpincl 37297 mzpf 37299 mzpindd 37309 rgspnmin 37741 clublem 37917 dftrcl3 38012 brtrclfv2 38019 dfrtrcl3 38025 intsaluni 40547 intsal 40548 salgenss 40554 salgencntex 40561 |
Copyright terms: Public domain | W3C validator |