![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > releldm | Structured version Visualization version GIF version |
Description: The first argument of a binary relation belongs to its domain. Note that 𝐴𝑅𝐵 does not imply Rel 𝑅: see for example nrelv 5519 and brv 5217. (Contributed by NM, 2-Jul-2008.) |
Ref | Expression |
---|---|
releldm | ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brrelex1 5451 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) | |
2 | brrelex2 5452 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) | |
3 | simpr 477 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵) | |
4 | breldmg 5624 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | |
5 | 1, 2, 3, 4 | syl3anc 1351 | 1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2050 Vcvv 3409 class class class wbr 4925 dom cdm 5403 Rel wrel 5408 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2744 ax-sep 5056 ax-nul 5063 ax-pr 5182 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-br 4926 df-opab 4988 df-xp 5409 df-rel 5410 df-dm 5413 |
This theorem is referenced by: releldmb 5656 releldmi 5658 sofld 5881 funeu 6210 fnbr 6289 funbrfv2b 6550 funfvbrb 6644 ercl 8098 inviso1 16906 setciso 17221 lmle 23619 dvidlem 24228 dvmulbr 24251 dvcobr 24258 ulmcau 24698 ulmdvlem3 24705 metideq 30806 heibor1lem 34558 rrncmslem 34581 eqvrelcl 35321 ntrclsiex 39795 ntrneiiex 39818 binomcxplemnn0 40126 binomcxplemnotnn0 40133 sumnnodd 41367 climlimsup 41497 climlimsupcex 41506 climliminflimsupd 41538 liminflimsupclim 41544 dmclimxlim 41588 xlimclimdm 41591 xlimresdm 41596 ioodvbdlimc1lem2 41672 ioodvbdlimc2lem 41674 funbrafv 42788 funbrafv2b 42789 rngciso 43642 rngcisoALTV 43654 ringciso 43693 ringcisoALTV 43717 |
Copyright terms: Public domain | W3C validator |