![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > intss1 | Structured version Visualization version GIF 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 3478 | . . . 4 ⊢ 𝑥 ∈ V | |
2 | 1 | elint 4955 | . . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦)) |
3 | eleq1 2821 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
4 | eleq2 2822 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴)) | |
5 | 3, 4 | imbi12d 344 | . . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
6 | 5 | spcgv 3586 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
7 | 6 | pm2.43a 54 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)) |
8 | 2, 7 | biimtrid 241 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴)) |
9 | 8 | ssrdv 3987 | 1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1539 = wceq 1541 ∈ wcel 2106 ⊆ wss 3947 ∩ cint 4949 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-in 3954 df-ss 3964 df-int 4950 |
This theorem is referenced by: intminss 4977 intmin3 4979 intab 4981 int0el 4982 trintss 5283 intex 5336 intidg 5456 oneqmini 6413 sorpssint 7719 onint 7774 onssmin 7776 onnmin 7782 nnawordex 8633 cofon1 8667 cofonr 8669 dffi2 9414 inficl 9416 dffi3 9422 tcmin 9732 tc2 9733 rankr1ai 9789 rankuni2b 9844 tcrank 9875 harval2 9988 cfflb 10250 fin23lem20 10328 fin23lem38 10340 isf32lem2 10345 intwun 10726 inttsk 10765 intgru 10805 dfnn2 12221 dfuzi 12649 trclubi 14939 trclubgi 14940 trclub 14941 trclubg 14942 cotrtrclfv 14955 trclun 14957 dfrtrcl2 15005 mremre 17544 isacs1i 17597 mrelatglb 18509 cycsubg 19079 efgrelexlemb 19612 efgcpbllemb 19617 frgpuplem 19634 primefld 20413 cssmre 21237 toponmre 22588 1stcfb 22940 ptcnplem 23116 fbssfi 23332 uffix 23416 ufildom1 23421 alexsublem 23539 alexsubALTlem4 23545 tmdgsum2 23591 bcth3 24839 limciun 25402 aalioulem3 25838 sltval2 27148 sltres 27154 nocvxminlem 27268 eqscut2 27296 scutun12 27300 scutbdaybnd 27305 scutbdaybnd2 27306 scutbdaylt 27308 madebdaylemlrcut 27382 cofcut1 27396 cofcutr 27400 shintcli 30569 shsval2i 30627 ococin 30648 chsupsn 30653 fldgensdrg 32392 fldgenssv 32393 fldgenssp 32396 insiga 33123 ldsysgenld 33146 ldgenpisyslem2 33150 mclsssvlem 34541 mclsax 34548 mclsind 34549 untint 34669 dfon2lem8 34750 dfon2lem9 34751 clsint2 35202 topmeet 35237 topjoin 35238 heibor1lem 36665 ismrcd1 41421 mzpincl 41457 mzpf 41459 mzpindd 41469 rgspnmin 41898 onintunirab 41961 oninfint 41970 clublem 42346 dftrcl3 42456 brtrclfv2 42463 dfrtrcl3 42469 intsaluni 45031 intsal 45032 salgenss 45038 salgencntex 45045 intubeu 47562 |
Copyright terms: Public domain | W3C validator |