Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssexi | Unicode version |
Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |
Ref | Expression |
---|---|
ssexi.1 | |
ssexi.2 |
Ref | Expression |
---|---|
ssexi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssexi.2 | . 2 | |
2 | ssexi.1 | . . 3 | |
3 | 2 | ssex 4113 | . 2 |
4 | 1, 3 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2135 cvv 2721 wss 3111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-sep 4094 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-in 3117 df-ss 3124 |
This theorem is referenced by: zfausab 4118 pp0ex 4162 ord3ex 4163 epse 4314 opabex 5703 oprabex 6088 phplem2 6810 phpm 6822 snexxph 6906 sbthlem2 6914 niex 7244 enqex 7292 enq0ex 7371 npex 7405 ltnqex 7481 gtnqex 7482 recexprlemell 7554 recexprlemelu 7555 enrex 7669 axcnex 7791 peano5nnnn 7824 reex 7878 nnex 8854 zex 9191 qex 9561 ixxex 9826 iccen 9933 serclim0 11232 climle 11261 iserabs 11402 isumshft 11417 explecnv 11432 prodfclim1 11471 prmex 12024 exmidunben 12296 istopon 12552 dmtopon 12562 lmres 12789 climcncf 13112 reldvg 13189 |
Copyright terms: Public domain | W3C validator |