![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > inss2 | 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 |
---|---|
inss2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | incom 3327 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | inss1 3355 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqsstrri 3188 |
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 2739 df-in 3135 df-ss 3142 |
This theorem is referenced by: difin0 3496 bnd2 4173 ordin 4385 relin2 4745 relres 4935 ssrnres 5071 cnvcnv 5081 funinsn 5265 funimaexg 5300 fnresin2 5331 ssimaex 5577 ffvresb 5679 ofrfval 6090 ofvalg 6091 ofrval 6092 off 6094 ofres 6096 ofco 6100 offres 6135 tpostpos 6264 smores3 6293 tfrlem5 6314 tfrexlem 6334 erinxp 6608 pmresg 6675 unfiin 6924 ltrelpi 7322 peano5nnnn 7890 peano5nni 8921 rexanuz 10996 structcnvcnv 12477 ressbasssd 12528 restsspw 12697 eltg4i 13491 ntrss2 13557 ntrin 13560 isopn3 13561 resttopon 13607 restuni2 13613 cnrest2r 13673 cnptopresti 13674 cnptoprest 13675 lmss 13682 metrest 13942 tgioo 13982 2sqlem8 14406 2sqlem9 14407 peano5set 14628 |
Copyright terms: Public domain | W3C validator |