![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssini | Structured version Visualization version GIF version |
Description: An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.) |
Ref | Expression |
---|---|
ssini.1 | ⊢ 𝐴 ⊆ 𝐵 |
ssini.2 | ⊢ 𝐴 ⊆ 𝐶 |
Ref | Expression |
---|---|
ssini | ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssini.1 | . . 3 ⊢ 𝐴 ⊆ 𝐵 | |
2 | ssini.2 | . . 3 ⊢ 𝐴 ⊆ 𝐶 | |
3 | 1, 2 | pm3.2i 470 | . 2 ⊢ (𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) |
4 | ssin 4222 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) | |
5 | 3, 4 | mpbi 229 | 1 ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 ∩ cin 3939 ⊆ wss 3940 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-v 3468 df-in 3947 df-ss 3957 |
This theorem is referenced by: inv1 4386 cnvrescnv 6184 hartogslem1 9533 xptrrel 14924 fbasrn 23710 limciun 25745 hlimcaui 30958 chdmm1i 31199 chm0i 31212 ledii 31258 lejdii 31260 mayetes3i 31451 mdslj2i 32042 mdslmd2i 32052 sumdmdlem2 32141 sigapildsys 33649 ssoninhaus 35823 bj-disj2r 36399 bj-idres 36531 bj-rvecsscvec 36675 icomnfinre 44750 fouriersw 45432 sge0split 45610 |
Copyright terms: Public domain | W3C validator |