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 3056 | . 2 | |
2 | ssriv.1 | . 2 | |
3 | 1, 2 | mpgbir 1414 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 wss 3041 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 |
This theorem is referenced by: ssid 3087 ssv 3089 difss 3172 ssun1 3209 inss1 3266 unssdif 3281 inssdif 3282 unssin 3285 inssun 3286 difindiss 3300 undif3ss 3307 0ss 3371 difprsnss 3628 snsspw 3661 pwprss 3702 pwtpss 3703 uniin 3726 iuniin 3793 iundif2ss 3848 iunpwss 3874 pwuni 4086 pwunss 4175 omsson 4496 limom 4497 xpsspw 4621 dmin 4717 dmrnssfld 4772 dmcoss 4778 dminss 4923 imainss 4924 dmxpss 4939 rnxpid 4943 mapsspm 6544 pmsspw 6545 uniixp 6583 snexxph 6806 djuss 6923 enq0enq 7207 nqnq0pi 7214 nqnq0 7217 apsscn 8377 sup3exmid 8683 zssre 9029 zsscn 9030 nnssz 9039 uzssz 9313 divfnzn 9381 zssq 9387 qssre 9390 rpssre 9420 ixxssxr 9651 ixxssixx 9653 iooval2 9666 ioossre 9686 rge0ssre 9728 fz1ssnn 9804 fzssuz 9813 fzssp1 9815 uzdisj 9841 fz0ssnn0 9864 nn0disj 9883 fzossfz 9910 fzouzsplit 9924 fzossnn 9934 fzo0ssnn0 9960 seq3coll 10553 fclim 11031 infssuzcldc 11571 prmssnn 11720 restsspw 12057 unitg 12158 cldss2 12202 blssioo 12641 tgioo 12642 limccl 12724 limcresi 12731 dvef 12783 bj-omsson 13087 |
Copyright terms: Public domain | W3C validator |