| 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 5810 and brv 5477. (Contributed by NM, 2-Jul-2008.) |
| Ref | Expression |
|---|---|
| releldm | ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brrelex1 5738 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) | |
| 2 | brrelex2 5739 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) | |
| 3 | simpr 484 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵) | |
| 4 | breldmg 5920 | . 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 395 ∈ wcel 2108 Vcvv 3480 class class class wbr 5143 dom cdm 5685 Rel wrel 5690 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-xp 5691 df-rel 5692 df-dm 5695 |
| This theorem is referenced by: releldmb 5957 releldmi 5959 sofld 6207 funeu 6591 fnbr 6676 funbrfv2b 6966 funfvbrb 7071 ercl 8756 inviso1 17810 setciso 18136 rngciso 20638 ringciso 20672 lmle 25335 dvidlem 25950 dvmulbr 25975 dvmulbrOLD 25976 dvcobr 25983 dvcobrOLD 25984 ulmcau 26438 ulmdvlem3 26445 metideq 33892 heibor1lem 37816 rrncmslem 37839 eqvrelcl 38613 ntrclsiex 44066 ntrneiiex 44089 binomcxplemnn0 44368 binomcxplemnotnn0 44375 sumnnodd 45645 climlimsup 45775 climlimsupcex 45784 climliminflimsupd 45816 liminflimsupclim 45822 dmclimxlim 45866 xlimclimdm 45869 xlimresdm 45874 ioodvbdlimc1lem2 45947 ioodvbdlimc2lem 45949 funbrafv 47170 funbrafv2b 47171 rngcisoALTV 48193 ringcisoALTV 48227 |
| Copyright terms: Public domain | W3C validator |