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 5670 and brv 5356. (Contributed by NM, 2-Jul-2008.) |
Ref | Expression |
---|---|
releldm | ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brrelex1 5602 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) | |
2 | brrelex2 5603 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) | |
3 | simpr 488 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵) | |
4 | breldmg 5778 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | |
5 | 1, 2, 3, 4 | syl3anc 1373 | 1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2110 Vcvv 3408 class class class wbr 5053 dom cdm 5551 Rel wrel 5556 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-br 5054 df-opab 5116 df-xp 5557 df-rel 5558 df-dm 5561 |
This theorem is referenced by: releldmb 5815 releldmi 5817 sofld 6050 funeu 6405 fnbr 6486 funbrfv2b 6770 funfvbrb 6871 ercl 8402 inviso1 17271 setciso 17597 lmle 24198 dvidlem 24812 dvmulbr 24836 dvcobr 24843 ulmcau 25287 ulmdvlem3 25294 metideq 31557 heibor1lem 35704 rrncmslem 35727 eqvrelcl 36462 ntrclsiex 41340 ntrneiiex 41363 binomcxplemnn0 41640 binomcxplemnotnn0 41647 sumnnodd 42846 climlimsup 42976 climlimsupcex 42985 climliminflimsupd 43017 liminflimsupclim 43023 dmclimxlim 43067 xlimclimdm 43070 xlimresdm 43075 ioodvbdlimc1lem2 43148 ioodvbdlimc2lem 43150 funbrafv 44322 funbrafv2b 44323 rngciso 45213 rngcisoALTV 45225 ringciso 45264 ringcisoALTV 45288 |
Copyright terms: Public domain | W3C validator |