| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > breldm | Structured version Visualization version GIF version | ||
| Description: Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.) |
| Ref | Expression |
|---|---|
| opeldm.1 | ⊢ 𝐴 ∈ V |
| opeldm.2 | ⊢ 𝐵 ∈ V |
| Ref | Expression |
|---|---|
| breldm | ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-br 5087 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
| 2 | opeldm.1 | . . 3 ⊢ 𝐴 ∈ V | |
| 3 | opeldm.2 | . . 3 ⊢ 𝐵 ∈ V | |
| 4 | 2, 3 | opeldm 5854 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ 𝑅 → 𝐴 ∈ dom 𝑅) |
| 5 | 1, 4 | sylbi 217 | 1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2114 Vcvv 3430 〈cop 4574 class class class wbr 5086 dom cdm 5622 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-rab 3391 df-v 3432 df-dif 3893 df-un 3895 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-br 5087 df-dm 5632 |
| This theorem is referenced by: imaindm 6255 funcnv3 6560 opabiota 6914 dffv2 6927 dff13 7200 exse2 7859 reldmtpos 8175 rntpos 8180 dftpos4 8186 tpostpos 8187 fprlem1 8241 iserd 8661 dmttrcl 9631 ttrclse 9637 frrlem15 9670 dcomex 10358 axdc2lem 10359 dmrecnq 10880 cotr2g 14900 shftfval 14994 geolim2 15795 geomulcvg 15800 geoisum1c 15804 cvgrat 15807 ntrivcvg 15821 eftlub 16035 eflegeo 16047 rpnnen2lem5 16144 imasleval 17463 psdmrn 18497 psssdm2 18505 ovoliunnul 25452 vitalilem5 25557 dvcj 25895 dvrec 25900 dvef 25925 ftc1cn 25991 aaliou3lem3 26292 ulmdv 26352 dvradcnv 26370 abelthlem7 26388 abelthlem9 26390 logtayllem 26608 leibpi 26892 log2tlbnd 26895 zetacvg 26965 hhcms 31263 hhsscms 31338 occl 31364 gsummpt2co 33114 iprodgam 35930 imageval 36116 knoppcnlem6 36756 knoppndvlem6 36775 knoppf 36793 unccur 37915 ftc1cnnc 38004 geomcau 38071 dvradcnv2 44777 xpco2 49290 |
| Copyright terms: Public domain | W3C validator |