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 3126 | . 2 | |
2 | ssriv.1 | . 2 | |
3 | 1, 2 | mpgbir 1440 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2135 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-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 |
This theorem is referenced by: ssid 3157 ssv 3159 difss 3243 ssun1 3280 inss1 3337 unssdif 3352 inssdif 3353 unssin 3356 inssun 3357 difindiss 3371 undif3ss 3378 0ss 3442 difprsnss 3705 snsspw 3738 pwprss 3779 pwtpss 3780 uniin 3803 iuniin 3870 iundif2ss 3925 iunpwss 3951 pwuni 4165 pwunss 4255 omsson 4584 limom 4585 xpsspw 4710 dmin 4806 dmrnssfld 4861 dmcoss 4867 dminss 5012 imainss 5013 dmxpss 5028 rnxpid 5032 mapsspm 6639 pmsspw 6640 uniixp 6678 snexxph 6906 djuss 7026 pw1on 7173 enq0enq 7363 nqnq0pi 7370 nqnq0 7373 apsscn 8536 sup3exmid 8843 zssre 9189 zsscn 9190 nnssz 9199 uzssz 9476 divfnzn 9550 zssq 9556 qssre 9559 rpssre 9591 ixxssxr 9827 ixxssixx 9829 iooval2 9842 ioossre 9862 rge0ssre 9904 fz1ssnn 9981 fzssuz 9990 fzssp1 9992 uzdisj 10018 fz0ssnn0 10041 nn0disj 10063 fzossfz 10090 fzouzsplit 10104 fzossnn 10114 fzo0ssnn0 10140 seq3coll 10741 fclim 11221 infssuzcldc 11869 prmssnn 12023 restsspw 12508 unitg 12609 cldss2 12653 blssioo 13092 tgioo 13093 limccl 13175 limcresi 13182 dvef 13235 reeff1o 13241 bj-omsson 13685 |
Copyright terms: Public domain | W3C validator |