| 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 3484 | . . . 4 ⊢ 𝑥 ∈ V | |
| 2 | 1 | elint 4952 | . . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦)) |
| 3 | eleq1 2829 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
| 4 | eleq2 2830 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴)) | |
| 5 | 3, 4 | imbi12d 344 | . . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
| 6 | 5 | spcgv 3596 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
| 7 | 6 | pm2.43a 54 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)) |
| 8 | 2, 7 | biimtrid 242 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴)) |
| 9 | 8 | ssrdv 3989 | 1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 = wceq 1540 ∈ wcel 2108 ⊆ wss 3951 ∩ cint 4946 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-int 4947 |
| This theorem is referenced by: intminss 4974 intmin3 4976 intab 4978 int0el 4979 trintss 5278 intex 5344 intidg 5462 oneqmini 6436 sorpssint 7753 onint 7810 onssmin 7812 onnmin 7818 nnawordex 8675 cofon1 8710 cofonr 8712 dffi2 9463 inficl 9465 dffi3 9471 tcmin 9781 tc2 9782 rankr1ai 9838 rankuni2b 9893 tcrank 9924 harval2 10037 cfflb 10299 fin23lem20 10377 fin23lem38 10389 isf32lem2 10394 intwun 10775 inttsk 10814 intgru 10854 dfnn2 12279 dfuzi 12709 trclubi 15035 trclubgi 15036 trclub 15037 trclubg 15038 cotrtrclfv 15051 trclun 15053 dfrtrcl2 15101 mremre 17647 isacs1i 17700 mrelatglb 18605 cycsubg 19226 efgrelexlemb 19768 efgcpbllemb 19773 frgpuplem 19790 rgspnmin 20615 primefld 20806 cssmre 21711 toponmre 23101 1stcfb 23453 ptcnplem 23629 fbssfi 23845 uffix 23929 ufildom1 23934 alexsublem 24052 alexsubALTlem4 24058 tmdgsum2 24104 bcth3 25365 limciun 25929 aalioulem3 26376 sltval2 27701 sltres 27707 nocvxminlem 27822 eqscut2 27851 scutun12 27855 scutbdaybnd 27860 scutbdaybnd2 27861 scutbdaylt 27863 madebdaylemlrcut 27937 cofcut1 27954 cofcutr 27958 dfn0s2 28336 shintcli 31348 shsval2i 31406 ococin 31427 chsupsn 31432 elrgspnlem4 33249 fldgensdrg 33316 fldgenssv 33317 fldgenssp 33320 insiga 34138 ldsysgenld 34161 ldgenpisyslem2 34165 mclsssvlem 35567 mclsax 35574 mclsind 35575 untint 35712 dfon2lem8 35791 dfon2lem9 35792 clsint2 36330 topmeet 36365 topjoin 36366 heibor1lem 37816 ismrcd1 42709 mzpincl 42745 mzpf 42747 mzpindd 42757 onintunirab 43239 oninfint 43248 clublem 43623 dftrcl3 43733 brtrclfv2 43740 dfrtrcl3 43746 intsaluni 46344 intsal 46345 salgenss 46351 salgencntex 46358 intubeu 48873 |
| Copyright terms: Public domain | W3C validator |