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 3176 | . . . 4 ⊢ 𝑥 ∈ V | |
2 | 1 | elint 4416 | . . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦)) |
3 | eleq1 2676 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
4 | eleq2 2677 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴)) | |
5 | 3, 4 | imbi12d 333 | . . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
6 | 5 | spcgv 3266 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
7 | 6 | pm2.43a 52 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)) |
8 | 2, 7 | syl5bi 231 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴)) |
9 | 8 | ssrdv 3574 | 1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 = wceq 1475 ∈ wcel 1977 ⊆ wss 3540 ∩ cint 4410 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 df-ss 3554 df-int 4411 |
This theorem is referenced by: intminss 4438 intmin3 4440 intab 4442 int0el 4443 trint0 4698 intex 4747 oneqmini 5693 sorpssint 6845 onint 6887 onssmin 6889 onnmin 6895 nnawordex 7604 dffi2 8212 inficl 8214 dffi3 8220 tcmin 8500 tc2 8501 rankr1ai 8544 rankuni2b 8599 tcrank 8630 harval2 8706 cfflb 8964 fin23lem20 9042 fin23lem38 9054 isf32lem2 9059 intwun 9436 inttsk 9475 intgru 9515 dfnn2 10910 dfuzi 11344 trclubi 13583 trclubiOLD 13584 trclubgi 13585 trclubgiOLD 13586 trclub 13587 trclubg 13588 cotrtrclfv 13601 trclun 13603 dfrtrcl2 13650 mremre 16087 isacs1i 16141 mrelatglb 17007 cycsubg 17445 efgrelexlemb 17986 efgcpbllemb 17991 frgpuplem 18008 cssmre 19856 toponmre 20707 1stcfb 21058 ptcnplem 21234 fbssfi 21451 uffix 21535 ufildom1 21540 alexsublem 21658 alexsubALTlem4 21664 tmdgsum2 21710 bcth3 22936 limciun 23464 aalioulem3 23893 shintcli 27572 shsval2i 27630 ococin 27651 chsupsn 27656 insiga 29527 ldsysgenld 29550 ldgenpisyslem2 29554 mclsssvlem 30713 mclsax 30720 mclsind 30721 untint 30843 dfon2lem8 30939 dfon2lem9 30940 sltval2 31053 sltres 31061 nodenselem7 31086 nocvxminlem 31089 nobndup 31099 nobnddown 31100 clsint2 31494 topmeet 31529 topjoin 31530 heibor1lem 32778 ismrcd1 36279 mzpincl 36315 mzpf 36317 mzpindd 36327 rgspnmin 36760 clublem 36936 dftrcl3 37031 brtrclfv2 37038 dfrtrcl3 37044 intsaluni 39223 intsal 39224 salgenss 39230 salgencntex 39237 |
Copyright terms: Public domain | W3C validator |