![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relss | Structured version Visualization version 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 3425 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-rel 4846 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df-rel 4846 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3imtr4g 278 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-in 3397 df-ss 3404 df-rel 4846 |
This theorem is referenced by: relin1 4956 relin2 4957 reldif 4958 relres 5138 iss 5158 cnvdif 5248 difxp 5267 sofld 5290 funss 5607 funssres 5629 fliftcnv 6222 fliftfun 6223 frxp 6925 reltpos 6996 tpostpos 7011 swoer 7409 erinxp 7455 sbthcl 7712 fpwwe2lem8 9080 fpwwe2lem9 9081 fpwwe2lem12 9084 recmulnq 9407 prcdnq 9436 ltrel 9714 lerel 9716 dfle2 11469 dflt2 11470 pwsle 15468 isinv 15743 invsym2 15746 invfun 15747 oppcsect2 15762 oppcinv 15763 relfull 15891 relfth 15892 psss 16538 gicer 17018 gsum2d 17682 isunit 17963 opsrtoslem2 18785 txdis1cn 20727 hmpher 20876 tgphaus 21209 qustgplem 21213 tsmsxp 21247 xmeter 21526 ovoliunlem1 22533 taylf 23395 lgsquadlem1 24361 lgsquadlem2 24362 nvrel 26302 phrel 26537 bnrel 26590 hlrel 26623 elrn3 30474 sscoid 30751 trer 31043 fneer 31080 heicant 32039 dvhopellsm 34756 diclspsn 34833 dih1dimatlem 34968 |
Copyright terms: Public domain | W3C validator |