![]() |
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 3343 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 274 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ssriv 3184 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-v 2762 df-in 3160 df-ss 3167 |
This theorem is referenced by: inss2 3381 ssinss1 3389 unabs 3391 inssddif 3401 inv1 3484 disjdif 3520 inundifss 3525 relin1 4778 resss 4967 resmpt3 4992 cnvcnvss 5121 funin 5326 funimass2 5333 fnresin1 5369 fnres 5371 fresin 5433 ssimaex 5619 fneqeql2 5668 isoini2 5863 ofrfval 6141 ofvalg 6142 ofrval 6143 off 6145 ofres 6147 ofco 6151 smores 6347 smores2 6349 tfrlem5 6369 pmresg 6732 unfiin 6984 infidc 6995 sbthlem7 7024 peano5nnnn 7954 peano5nni 8987 rexanuz 11135 nninfdclemcl 12608 nninfdclemp1 12610 fvsetsid 12655 tgvalex 12877 tgval2 14230 eltg3 14236 tgcl 14243 tgdom 14251 tgidm 14253 epttop 14269 ntropn 14296 ntrin 14303 cnptopresti 14417 cnptoprest 14418 txcnmpt 14452 xmetres 14561 metres 14562 blin2 14611 metrest 14685 tgioo 14733 limcresi 14845 2sqlem8 15280 bj-charfun 15369 bj-charfundc 15370 bj-charfundcALT 15371 |
Copyright terms: Public domain | W3C validator |