![]() |
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 3320 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 274 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ssriv 3161 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2741 df-in 3137 df-ss 3144 |
This theorem is referenced by: inss2 3358 ssinss1 3366 unabs 3368 inssddif 3378 inv1 3461 disjdif 3497 inundifss 3502 relin1 4746 resss 4933 resmpt3 4958 cnvcnvss 5085 funin 5289 funimass2 5296 fnresin1 5332 fnres 5334 fresin 5396 ssimaex 5579 fneqeql2 5627 isoini2 5822 ofrfval 6093 ofvalg 6094 ofrval 6095 off 6097 ofres 6099 ofco 6103 smores 6295 smores2 6297 tfrlem5 6317 pmresg 6678 unfiin 6927 sbthlem7 6964 peano5nnnn 7893 peano5nni 8924 rexanuz 10999 nninfdclemcl 12451 nninfdclemp1 12453 fvsetsid 12498 tgvalex 12717 tgval2 13636 eltg3 13642 tgcl 13649 tgdom 13657 tgidm 13659 epttop 13675 ntropn 13702 ntrin 13709 cnptopresti 13823 cnptoprest 13824 txcnmpt 13858 xmetres 13967 metres 13968 blin2 14017 metrest 14091 tgioo 14131 limcresi 14220 2sqlem8 14555 bj-charfun 14644 bj-charfundc 14645 bj-charfundcALT 14646 |
Copyright terms: Public domain | W3C validator |