![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssbrd | Structured version Visualization version Unicode version |
Description: Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.) |
Ref | Expression |
---|---|
ssbrd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ssbrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssbrd.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | sseld 3417 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-br 4396 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-br 4396 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 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-br 4396 |
This theorem is referenced by: ssbri 4438 sess1 4807 brrelex12 4877 coss1 4995 coss2 4996 eqbrrdva 5009 ersym 7393 ertr 7396 fpwwe2lem6 9078 fpwwe2lem7 9079 fpwwe2lem9 9081 fpwwe2lem12 9084 fpwwe2lem13 9085 fpwwe2 9086 coss12d 13111 fthres2 15915 invfuc 15957 pospo 16297 dirref 16559 efgcpbl 17484 frgpuplem 17500 subrguss 18101 znleval 19202 ustref 21311 ustuqtop4 21337 isucn2 21372 brelg 28293 metider 28771 mclsppslem 30293 fundmpss 30478 iunrelexpuztr 36382 frege96d 36412 frege91d 36414 frege98d 36416 frege124d 36424 ssrelrn 39156 |
Copyright terms: Public domain | W3C validator |