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 3629 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥)) | |
2 | 1 | ss2abdv 3638 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} ⊆ {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}) |
3 | dfint2 4412 | . 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} | |
4 | dfint2 4412 | . 2 ⊢ ∩ 𝐴 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
5 | 2, 3, 4 | 3sstr4g 3609 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 {cab 2596 ∀wral 2896 ⊆ 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-ral 2901 df-in 3547 df-ss 3554 df-int 4411 |
This theorem is referenced by: uniintsn 4449 intabs 4752 fiss 8213 tc2 8501 tcss 8503 tcel 8504 rankval4 8613 cfub 8954 cflm 8955 cflecard 8958 fin23lem26 9030 clsslem 13571 mrcss 16099 lspss 18805 lbsextlem3 18981 aspss 19153 clsss 20668 1stcfb 21058 ufinffr 21543 spanss 27591 ss2mcls 30719 pclssN 34198 dochspss 35685 clss2lem 36937 |
Copyright terms: Public domain | W3C validator |