![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ssexg | Unicode version |
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
ssexg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq2 3063 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | imbi1d 230 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | vex 2636 |
. . . 4
![]() ![]() ![]() ![]() | |
4 | 3 | ssex 3997 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | vtoclg 2693 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | impcom 124 |
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 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-in 3019 df-ss 3026 |
This theorem is referenced by: ssexd 4000 difexg 4001 rabexg 4003 elssabg 4005 elpw2g 4013 abssexg 4038 snexg 4040 sess1 4188 sess2 4189 trsuc 4273 unexb 4292 abnexg 4296 uniexb 4323 xpexg 4581 riinint 4726 dmexg 4729 rnexg 4730 resexg 4785 resiexg 4790 imaexg 4819 exse2 4839 cnvexg 5002 coexg 5009 fabexg 5233 f1oabexg 5300 relrnfvex 5358 fvexg 5359 sefvex 5361 mptfvex 5424 mptexg 5561 ofres 5907 resfunexgALT 5919 cofunexg 5920 fnexALT 5922 f1dmex 5925 oprabexd 5936 mpt2exxg 6015 tposexg 6061 frecabex 6201 erex 6356 mapex 6451 pmvalg 6456 elpmg 6461 elmapssres 6470 pmss12g 6472 ixpexgg 6519 ssdomg 6575 fiprc 6612 shftfvalg 10367 shftfval 10370 toponsspwpwg 11872 tgval 11901 tgvalex 11902 eltg 11904 eltg2 11905 tgss 11915 basgen2 11933 bastop1 11935 topnex 11938 resttopon 12023 restabs 12027 lmfval 12044 cnrest 12086 metrest 12292 |
Copyright terms: Public domain | W3C validator |