Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > relss | Unicode version |
Description: Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.) |
Ref | Expression |
---|---|
relss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 3135 | . 2 | |
2 | df-rel 4593 | . 2 | |
3 | df-rel 4593 | . 2 | |
4 | 1, 2, 3 | 3imtr4g 204 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 cvv 2712 wss 3102 cxp 4584 wrel 4591 |
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 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-11 1486 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-in 3108 df-ss 3115 df-rel 4593 |
This theorem is referenced by: relin1 4704 relin2 4705 reldif 4706 relres 4894 iss 4912 cnvdif 4992 funss 5189 funssres 5212 fliftcnv 5745 fliftfun 5746 reltpos 6197 tpostpos 6211 swoer 6508 erinxp 6554 ltrel 7939 lerel 7941 txdis1cn 12678 xmeter 12836 |
Copyright terms: Public domain | W3C validator |