|   | 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 4051 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥)) | |
| 2 | 1 | ss2abdv 4065 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} ⊆ {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}) | 
| 3 | dfint2 4947 | . 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} | |
| 4 | dfint2 4947 | . 2 ⊢ ∩ 𝐴 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
| 5 | 2, 3, 4 | 3sstr4g 4036 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 {cab 2713 ∀wral 3060 ⊆ wss 3950 ∩ cint 4945 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-ral 3061 df-ss 3967 df-int 4946 | 
| This theorem is referenced by: uniintsn 4984 intabs 5348 cofon1 8711 naddssim 8724 fiss 9465 tc2 9783 tcss 9785 tcel 9786 rankval4 9908 cfub 10290 cflm 10291 cflecard 10294 fin23lem26 10366 clsslem 15024 mrcss 17660 lspss 20983 lbsextlem3 21163 aspss 21898 clsss 23063 1stcfb 23454 ufinffr 23938 cofcut1 27955 spanss 31368 fldgenss 33319 ss2mcls 35574 pclssN 39897 dochspss 41381 clss2lem 43629 | 
| Copyright terms: Public domain | W3C validator |