![]() |
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 3799 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥)) | |
2 | 1 | ss2abdv 3808 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} ⊆ {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}) |
3 | dfint2 4621 | . 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} | |
4 | dfint2 4621 | . 2 ⊢ ∩ 𝐴 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
5 | 2, 3, 4 | 3sstr4g 3779 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 {cab 2738 ∀wral 3042 ⊆ wss 3707 ∩ cint 4619 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ral 3047 df-in 3714 df-ss 3721 df-int 4620 |
This theorem is referenced by: uniintsn 4658 intabs 4966 fiss 8487 tc2 8783 tcss 8785 tcel 8786 rankval4 8895 cfub 9255 cflm 9256 cflecard 9259 fin23lem26 9331 clsslem 13916 mrcss 16470 lspss 19178 lbsextlem3 19354 aspss 19526 clsss 21052 1stcfb 21442 ufinffr 21926 spanss 28508 ss2mcls 31764 pclssN 35675 dochspss 37161 clss2lem 38412 |
Copyright terms: Public domain | W3C validator |