Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > releldmi | Structured version Visualization version GIF version |
Description: The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.) |
Ref | Expression |
---|---|
releldm.1 | ⊢ Rel 𝑅 |
Ref | Expression |
---|---|
releldmi | ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | releldm.1 | . 2 ⊢ Rel 𝑅 | |
2 | releldm 5817 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | |
3 | 1, 2 | mpan 688 | 1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2113 class class class wbr 5069 dom cdm 5558 Rel wrel 5563 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pr 5333 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ral 3146 df-rex 3147 df-rab 3150 df-v 3499 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-br 5070 df-opab 5132 df-xp 5564 df-rel 5565 df-dm 5568 |
This theorem is referenced by: fpwwe2lem11 10065 fpwwe2lem12 10066 fpwwe2lem13 10067 rlimpm 14860 rlimdm 14911 iserex 15016 caucvgrlem2 15034 caucvgr 15035 caurcvg2 15037 caucvg 15038 fsumcvg3 15089 cvgcmpce 15176 climcnds 15209 trirecip 15221 ledm 17837 cmetcaulem 23894 ovoliunlem1 24106 mbflimlem 24271 dvaddf 24542 dvmulf 24543 dvcof 24548 dvcnv 24577 abelthlem5 25026 emcllem6 25581 lgamgulmlem4 25612 hlimcaui 29016 brfvrcld2 40043 sumnnodd 41917 climliminf 42093 stirlinglem12 42377 fouriersw 42523 rlimdmafv 43383 rlimdmafv2 43464 |
Copyright terms: Public domain | W3C validator |