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 474 | . 2 ⊢ (𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) |
4 | ssin 4119 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) | |
5 | 3, 4 | mpbi 233 | 1 ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 ∩ cin 3840 ⊆ wss 3841 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 df-in 3848 df-ss 3858 |
This theorem is referenced by: inv1 4280 cnvrescnv 6021 hartogslem1 9072 xptrrel 14422 fbasrn 22628 limciun 24638 hlimcaui 29163 chdmm1i 29404 chm0i 29417 ledii 29463 lejdii 29465 mayetes3i 29656 mdslj2i 30247 mdslmd2i 30257 sumdmdlem2 30346 sigapildsys 31692 ssoninhaus 34267 bj-disj2r 34830 bj-idres 34941 bj-rvecsscvec 35084 icomnfinre 42614 fouriersw 43298 sge0split 43473 |
Copyright terms: Public domain | W3C validator |