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 3412 | . . . 4 ⊢ 𝑥 ∈ V | |
2 | 1 | elint 4865 | . . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦)) |
3 | eleq1 2825 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
4 | eleq2 2826 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴)) | |
5 | 3, 4 | imbi12d 348 | . . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
6 | 5 | spcgv 3511 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
7 | 6 | pm2.43a 54 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)) |
8 | 2, 7 | syl5bi 245 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴)) |
9 | 8 | ssrdv 3907 | 1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1541 = wceq 1543 ∈ wcel 2110 ⊆ wss 3866 ∩ cint 4859 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-in 3873 df-ss 3883 df-int 4860 |
This theorem is referenced by: intminss 4885 intmin3 4887 intab 4889 int0el 4890 trintss 5178 intex 5230 oneqmini 6264 sorpssint 7521 onint 7574 onssmin 7576 onnmin 7582 nnawordex 8365 dffi2 9039 inficl 9041 dffi3 9047 tcmin 9357 tc2 9358 rankr1ai 9414 rankuni2b 9469 tcrank 9500 harval2 9613 cfflb 9873 fin23lem20 9951 fin23lem38 9963 isf32lem2 9968 intwun 10349 inttsk 10388 intgru 10428 dfnn2 11843 dfuzi 12268 trclubi 14559 trclubgi 14560 trclub 14561 trclubg 14562 cotrtrclfv 14575 trclun 14577 dfrtrcl2 14625 mremre 17107 isacs1i 17160 mrelatglb 18066 cycsubg 18615 efgrelexlemb 19140 efgcpbllemb 19145 frgpuplem 19162 primefld 19849 cssmre 20655 toponmre 21990 1stcfb 22342 ptcnplem 22518 fbssfi 22734 uffix 22818 ufildom1 22823 alexsublem 22941 alexsubALTlem4 22947 tmdgsum2 22993 bcth3 24228 limciun 24791 aalioulem3 25227 shintcli 29410 shsval2i 29468 ococin 29489 chsupsn 29494 insiga 31817 ldsysgenld 31840 ldgenpisyslem2 31844 mclsssvlem 33237 mclsax 33244 mclsind 33245 untint 33366 dfon2lem8 33485 dfon2lem9 33486 sltval2 33596 sltres 33602 nocvxminlem 33709 eqscut2 33737 scutun12 33741 scutbdaybnd 33746 scutbdaybnd2 33747 scutbdaylt 33749 madebdaylemlrcut 33816 cofcut1 33827 cofcutr 33829 clsint2 34255 topmeet 34290 topjoin 34291 heibor1lem 35704 ismrcd1 40223 mzpincl 40259 mzpf 40261 mzpindd 40271 rgspnmin 40699 clublem 40894 dftrcl3 41005 brtrclfv2 41012 dfrtrcl3 41018 intsaluni 43543 intsal 43544 salgenss 43550 salgencntex 43557 intubeu 45943 |
Copyright terms: Public domain | W3C validator |