![]() |
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 3052 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssriv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpgbir 1412 |
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-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-11 1467 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-in 3043 df-ss 3050 |
This theorem is referenced by: ssid 3083 ssv 3085 difss 3168 ssun1 3205 inss1 3262 unssdif 3277 inssdif 3278 unssin 3281 inssun 3282 difindiss 3296 undif3ss 3303 0ss 3367 difprsnss 3624 snsspw 3657 pwprss 3698 pwtpss 3699 uniin 3722 iuniin 3789 iundif2ss 3844 iunpwss 3870 pwuni 4076 pwunss 4165 omsson 4486 limom 4487 xpsspw 4611 dmin 4707 dmrnssfld 4760 dmcoss 4766 dminss 4911 imainss 4912 dmxpss 4927 rnxpid 4931 mapsspm 6530 pmsspw 6531 uniixp 6569 snexxph 6790 djuss 6907 enq0enq 7187 nqnq0pi 7194 nqnq0 7197 sup3exmid 8625 zssre 8965 zsscn 8966 nnssz 8975 uzssz 9247 divfnzn 9315 zssq 9321 qssre 9324 rpssre 9353 ixxssxr 9576 ixxssixx 9578 iooval2 9591 ioossre 9611 rge0ssre 9653 fz1ssnn 9729 fzssuz 9738 fzssp1 9740 uzdisj 9766 fz0ssnn0 9789 nn0disj 9808 fzossfz 9835 fzouzsplit 9849 fzossnn 9859 fzo0ssnn0 9885 seq3coll 10478 fclim 10955 infssuzcldc 11492 prmssnn 11639 restsspw 11973 unitg 12074 cldss2 12118 blssioo 12531 tgioo 12532 limccl 12584 limcresi 12591 bj-omsson 12852 |
Copyright terms: Public domain | W3C validator |