| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > intss | Structured version Visualization version GIF version | ||
| Description: Intersection of subclasses. (Contributed by NM, 14-Oct-1999.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| Ref | Expression |
|---|---|
| intss | ⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssralv 4008 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥)) | |
| 2 | 1 | ss2abdv 4021 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} ⊆ {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}) |
| 3 | dfint2 4909 | . 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} | |
| 4 | dfint2 4909 | . 2 ⊢ ∩ 𝐴 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
| 5 | 2, 3, 4 | 3sstr4g 3992 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 {cab 2743 ∀wral 3079 ⊆ wss 3907 ∩ cint 4907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-ral 3080 df-ss 3924 df-int 4908 |
| This theorem is referenced by: uniintsn 4945 intabs 5309 cofon1 8646 naddssim 8660 fiss 9372 tc2 9697 tcss 9699 tcel 9700 rankval4 9827 cfub 10220 cflm 10221 cflecard 10224 fin23lem26 10297 clsslem 15009 mrcss 17660 lspss 21071 lbsextlem3 21250 aspss 21983 clsss 23168 1stcfb 23559 ufinffr 24043 cofcut1 28067 spanss 31605 fldgenss 33547 rankval4b 35403 ss2mcls 35926 pclssN 40525 dochspss 42009 clss2lem 44194 |
| Copyright terms: Public domain | W3C validator |