![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > releldm | Structured version Unicode version |
Description: The first argument of a binary relation belongs to its domain. (Contributed by NM, 2-Jul-2008.) |
Ref | Expression |
---|---|
releldm |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brrelex 4977 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | brrelex2 4978 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | simpr 461 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | breldmg 5145 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | syl3anc 1219 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4513 ax-nul 4521 ax-pr 4631 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-rab 2804 df-v 3072 df-dif 3431 df-un 3433 df-in 3435 df-ss 3442 df-nul 3738 df-if 3892 df-sn 3978 df-pr 3980 df-op 3984 df-br 4393 df-opab 4451 df-xp 4946 df-rel 4947 df-dm 4950 |
This theorem is referenced by: releldmb 5174 releldmi 5176 sofld 5386 funeu 5542 fnbr 5613 funbrfv2b 5837 funfvbrb 5917 ercl 7214 inviso1 14808 setciso 15063 lmle 20930 dvidlem 21508 dvmulbr 21531 dvcobr 21538 ulmcau 21978 ulmdvlem3 21985 uhgraun 23382 umgraun 23399 metideq 26456 heibor1lem 28848 rrncmslem 28871 funbrafv 30204 funbrafv2b 30205 |
Copyright terms: Public domain | W3C validator |