Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reldmmpt2 | Structured version Visualization version Unicode version |
Description: The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
Ref | Expression |
---|---|
rngop.1 |
Ref | Expression |
---|---|
reldmmpt2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reldmoprab 6745 | . 2 | |
2 | rngop.1 | . . . . 5 | |
3 | df-mpt2 6655 | . . . . 5 | |
4 | 2, 3 | eqtri 2644 | . . . 4 |
5 | 4 | dmeqi 5325 | . . 3 |
6 | 5 | releqi 5202 | . 2 |
7 | 1, 6 | mpbir 221 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wa 384 wceq 1483 wcel 1990 cdm 5114 wrel 5119 coprab 6651 cmpt2 6652 |
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 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-xp 5120 df-rel 5121 df-dm 5124 df-oprab 6654 df-mpt2 6655 |
This theorem is referenced by: reldmmap 7866 reldmsets 15886 reldmress 15926 reldmprds 16109 gsum0 17278 reldmghm 17659 oppglsm 18057 reldmdprd 18396 reldmlmhm 19025 reldmpsr 19361 reldmmpl 19427 reldmopsr 19473 reldmevls 19517 vr1val 19562 reldmevls1 19682 evl1fval 19692 zrhval 19856 reldmdsmm 20077 frlmrcl 20101 matbas0pc 20215 mdetfval 20392 madufval 20443 qtopres 21501 fgabs 21683 reldmtng 22442 reldmnghm 22516 reldmnmhm 22517 dvbsss 23666 reldmmdeg 23817 nbgrprc0 26229 wwlksn 26729 wwlks2onv 26847 clwwlksn 26881 reldmresv 29826 bj-restsnid 33040 mzpmfp 37310 brovmptimex 38325 |
Copyright terms: Public domain | W3C validator |