![]() |
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 1778 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | relssdv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | ssrel 4901 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | syl 17 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 5 | mpbird 240 |
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 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-sep 4497 ax-nul 4506 ax-pr 4612 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-v 3015 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-if 3850 df-sn 3937 df-pr 3939 df-op 3943 df-opab 4434 df-xp 4818 df-rel 4819 |
This theorem is referenced by: relssres 5120 poirr2 5202 sofld 5262 relssdmrn 5335 funcres2 15814 wunfunc 15815 fthres2 15848 pospo 16230 joindmss 16264 meetdmss 16278 clatl 16373 subrgdvds 18033 opsrtoslem2 18719 txcls 20630 txdis1cn 20661 txkgen 20678 qustgplem 21146 metustid 21580 metustexhalf 21582 ovoliunlem1 22466 dvres2 22879 cvmlift2lem12 30043 dib2dim 34813 dih2dimbALTN 34815 dihmeetlem1N 34860 dihglblem5apreN 34861 dihmeetlem13N 34889 dihjatcclem4 34991 |
Copyright terms: Public domain | W3C validator |