![]() |
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 3438 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-rel 4840 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df-rel 4840 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3imtr4g 274 |
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 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-in 3410 df-ss 3417 df-rel 4840 |
This theorem is referenced by: relin1 4950 relin2 4951 reldif 4952 relres 5131 iss 5151 cnvdif 5241 difxp 5260 sofld 5283 funss 5599 funssres 5621 fliftcnv 6202 fliftfun 6203 frxp 6903 reltpos 6975 tpostpos 6990 swoer 7388 erinxp 7434 sbthcl 7691 fpwwe2lem8 9059 fpwwe2lem9 9060 fpwwe2lem12 9063 recmulnq 9386 prcdnq 9415 ltrel 9693 lerel 9695 dfle2 11443 dflt2 11444 pwsle 15383 isinv 15658 invsym2 15661 invfun 15662 oppcsect2 15677 oppcinv 15678 relfull 15806 relfth 15807 psss 16453 gicer 16933 gsum2d 17597 isunit 17878 opsrtoslem2 18701 txdis1cn 20643 hmpher 20792 tgphaus 21124 qustgplem 21128 tsmsxp 21162 xmeter 21441 ovoliunlem1 22448 taylf 23309 lgsquadlem1 24275 lgsquadlem2 24276 nvrel 26214 phrel 26449 bnrel 26502 hlrel 26535 elrn3 30396 sscoid 30673 trer 30965 fneer 31002 heicant 31968 dvhopellsm 34679 diclspsn 34756 dih1dimatlem 34891 |
Copyright terms: Public domain | W3C validator |