Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > relssdv | Structured version Visualization version Unicode version |
Description: Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.) |
Ref | Expression |
---|---|
relssdv.1 | |
relssdv.2 |
Ref | Expression |
---|---|
relssdv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relssdv.2 | . . 3 | |
2 | 1 | alrimivv 1856 | . 2 |
3 | relssdv.1 | . . 3 | |
4 | ssrel 5207 | . . 3 | |
5 | 3, 4 | syl 17 | . 2 |
6 | 2, 5 | mpbird 247 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wal 1481 wcel 1990 wss 3574 cop 4183 wrel 5119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-in 3581 df-ss 3588 df-opab 4713 df-xp 5120 df-rel 5121 |
This theorem is referenced by: relssres 5437 poirr2 5520 sofld 5581 relssdmrn 5656 funcres2 16558 wunfunc 16559 fthres2 16592 pospo 16973 joindmss 17007 meetdmss 17021 clatl 17116 subrgdvds 18794 opsrtoslem2 19485 txcls 21407 txdis1cn 21438 txkgen 21455 qustgplem 21924 metustid 22359 metustexhalf 22361 ovoliunlem1 23270 dvres2 23676 cvmlift2lem12 31296 dib2dim 36532 dih2dimbALTN 36534 dihmeetlem1N 36579 dihglblem5apreN 36580 dihmeetlem13N 36608 dihjatcclem4 36710 |
Copyright terms: Public domain | W3C validator |