![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ssrab2 | Unicode version |
Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.) |
Ref | Expression |
---|---|
ssrab2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rab 2397 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssab2 3145 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqsstri 3093 |
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 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-rab 2397 df-in 3041 df-ss 3048 |
This theorem is referenced by: ssrabeq 3147 rabexg 4029 pwnss 4041 undifexmid 4075 exmidexmid 4078 exmidsssnc 4084 onintrab2im 4392 ordtriexmidlem 4393 ontr2exmid 4398 ordtri2or2exmidlem 4399 onsucsssucexmid 4400 onsucelsucexmidlem 4402 tfis 4455 nnregexmid 4492 dmmptss 4991 ssimaex 5434 f1oresrab 5537 riotacl 5696 pmvalg 6505 ssfiexmid 6721 domfiexmid 6723 ctssdccl 6946 ctssexmid 6972 genpelxp 7261 ltexprlempr 7358 cauappcvgprlemcl 7403 cauappcvgprlemladd 7408 caucvgprlemcl 7426 caucvgprprlemcl 7454 uzf 9225 supminfex 9288 rpre 9343 ixxf 9568 fzf 9681 expcl2lemap 10192 expclzaplem 10204 expge0 10216 expge1 10217 dvdsflip 11391 infssuzex 11484 infssuzcldc 11486 gcddvds 11494 lcmn0cl 11589 phicl2 11729 phimullem 11740 ennnfonelemg 11755 ennnfonelemh 11756 ctiunctlemuom 11786 epttop 12096 neipsm 12160 cnpfval 12201 blfvalps 12368 blfps 12392 blf 12393 divcnap 12535 cdivcncfap 12567 limcdifap 12581 dvfgg 12606 dvidlemap 12609 dvcnp2cntop 12612 dvaddxxbr 12614 bdrabexg 12787 |
Copyright terms: Public domain | W3C validator |