![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ssriv | Unicode version |
Description: Inference based on subclass definition. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
ssriv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ssriv |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss2 3159 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssriv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpgbir 1464 |
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-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-in 3150 df-ss 3157 |
This theorem is referenced by: ssid 3190 ssv 3192 difss 3276 ssun1 3313 inss1 3370 unssdif 3385 inssdif 3386 unssin 3389 inssun 3390 difindiss 3404 undif3ss 3411 0ss 3476 difprsnss 3745 snsspw 3779 pwprss 3820 pwtpss 3821 uniin 3844 iuniin 3911 iundif2ss 3967 iunpwss 3993 pwuni 4210 pwunss 4301 omsson 4630 limom 4631 xpsspw 4756 dmin 4853 dmrnssfld 4908 dmcoss 4914 dminss 5061 imainss 5062 dmxpss 5077 rnxpid 5081 mapsspm 6708 pmsspw 6709 uniixp 6747 snexxph 6979 djuss 7099 pw1on 7255 enq0enq 7460 nqnq0pi 7467 nqnq0 7470 apsscn 8634 aptap 8637 sup3exmid 8944 zssre 9290 zsscn 9291 nnssz 9300 uzssz 9577 divfnzn 9651 zssq 9657 qssre 9660 rpssre 9694 ixxssxr 9930 ixxssixx 9932 iooval2 9945 ioossre 9965 rge0ssre 10007 fz1ssnn 10086 fzssuz 10095 fzssp1 10097 uzdisj 10123 fz0ssnn0 10146 nn0disj 10168 fzossfz 10195 fzouzsplit 10209 fzossnn 10219 fzo0ssnn0 10245 seq3coll 10854 fclim 11334 infssuzcldc 11984 prmssnn 12144 4sqlem19 12441 restsspw 12754 ringssrng 13391 subrngintm 13559 subrgintm 13590 cnsubmlem 13881 cnsubglem 13882 unitg 14019 cldss2 14063 blssioo 14502 tgioo 14503 limccl 14585 limcresi 14592 dvef 14645 reeff1o 14651 bj-omsson 15172 |
Copyright terms: Public domain | W3C validator |