![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > inss1 | Unicode version |
Description: The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
inss1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 3206 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 270 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ssriv 3051 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-v 2643 df-in 3027 df-ss 3034 |
This theorem is referenced by: inss2 3244 ssinss1 3252 unabs 3254 inssddif 3264 inv1 3346 disjdif 3382 inundifss 3387 relin1 4595 resss 4779 resmpt3 4804 cnvcnvss 4929 funin 5130 funimass2 5137 fnresin1 5173 fnres 5175 fresin 5237 ssimaex 5414 fneqeql2 5461 isoini2 5652 ofrfval 5922 fnofval 5923 ofrval 5924 off 5926 ofres 5927 ofco 5931 smores 6119 smores2 6121 tfrlem5 6141 pmresg 6500 unfiin 6743 sbthlem7 6779 peano5nnnn 7577 peano5nni 8581 rexanuz 10600 fvsetsid 11775 tgvalex 12001 tgval2 12002 eltg3 12008 tgcl 12015 tgdom 12023 tgidm 12025 epttop 12041 ntropn 12068 ntrin 12075 cnptopresti 12188 cnptoprest 12189 txcnmpt 12223 xmetres 12310 metres 12311 blin2 12360 metrest 12434 tgioo 12465 limcresi 12515 |
Copyright terms: Public domain | W3C validator |