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 3495 | . . . 4 ⊢ 𝑥 ∈ V | |
2 | 1 | elint 4873 | . . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦)) |
3 | eleq1 2897 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
4 | eleq2 2898 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴)) | |
5 | 3, 4 | imbi12d 346 | . . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
6 | 5 | spcgv 3592 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
7 | 6 | pm2.43a 54 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)) |
8 | 2, 7 | syl5bi 243 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴)) |
9 | 8 | ssrdv 3970 | 1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 = wceq 1528 ∈ wcel 2105 ⊆ wss 3933 ∩ cint 4867 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-in 3940 df-ss 3949 df-int 4868 |
This theorem is referenced by: intminss 4893 intmin3 4895 intab 4897 int0el 4898 trintss 5180 intex 5231 oneqmini 6235 sorpssint 7448 onint 7499 onssmin 7501 onnmin 7507 nnawordex 8252 dffi2 8875 inficl 8877 dffi3 8883 tcmin 9171 tc2 9172 rankr1ai 9215 rankuni2b 9270 tcrank 9301 harval2 9414 cfflb 9669 fin23lem20 9747 fin23lem38 9759 isf32lem2 9764 intwun 10145 inttsk 10184 intgru 10224 dfnn2 11639 dfuzi 12061 trclubi 14344 trclubgi 14345 trclub 14346 trclubg 14347 cotrtrclfv 14360 trclun 14362 dfrtrcl2 14409 mremre 16863 isacs1i 16916 mrelatglb 17782 cycsubg 18289 efgrelexlemb 18805 efgcpbllemb 18810 frgpuplem 18827 primefld 19513 cssmre 20765 toponmre 21629 1stcfb 21981 ptcnplem 22157 fbssfi 22373 uffix 22457 ufildom1 22462 alexsublem 22580 alexsubALTlem4 22586 tmdgsum2 22632 bcth3 23861 limciun 24419 aalioulem3 24850 shintcli 29033 shsval2i 29091 ococin 29112 chsupsn 29117 insiga 31295 ldsysgenld 31318 ldgenpisyslem2 31322 mclsssvlem 32706 mclsax 32713 mclsind 32714 untint 32835 dfon2lem8 32932 dfon2lem9 32933 sltval2 33060 sltres 33066 nocvxminlem 33144 scutun12 33168 scutbdaybnd 33172 scutbdaylt 33173 clsint2 33574 topmeet 33609 topjoin 33610 heibor1lem 34968 ismrcd1 39173 mzpincl 39209 mzpf 39211 mzpindd 39221 rgspnmin 39649 clublem 39848 dftrcl3 39943 brtrclfv2 39950 dfrtrcl3 39956 intsaluni 42489 intsal 42490 salgenss 42496 salgencntex 42503 |
Copyright terms: Public domain | W3C validator |