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 4032 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥)) | |
2 | 1 | ss2abdv 4043 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} ⊆ {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}) |
3 | dfint2 4870 | . 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} | |
4 | dfint2 4870 | . 2 ⊢ ∩ 𝐴 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
5 | 2, 3, 4 | 3sstr4g 4011 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 {cab 2799 ∀wral 3138 ⊆ wss 3935 ∩ cint 4868 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-in 3942 df-ss 3951 df-int 4869 |
This theorem is referenced by: uniintsn 4905 intabs 5237 fiss 8882 tc2 9178 tcss 9180 tcel 9181 rankval4 9290 cfub 9665 cflm 9666 cflecard 9669 fin23lem26 9741 clsslem 14338 mrcss 16881 lspss 19750 lbsextlem3 19926 aspss 20100 clsss 21656 1stcfb 22047 ufinffr 22531 spanss 29119 ss2mcls 32810 pclssN 37024 dochspss 38508 clss2lem 39964 |
Copyright terms: Public domain | W3C validator |