breldm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > breldm		Structured version Visualization version GIF version

Theorem breldm 5933

Description: Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)

**Hypotheses**
Ref	Expression
opeldm.1	⊢ 𝐴 ∈ V
opeldm.2	⊢ 𝐵 ∈ V

**Assertion**
Ref	Expression
breldm	⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

**Proof of Theorem breldm**
Step	Hyp	Ref	Expression
1		df-br 5167	. 2 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2		opeldm.1	. . 3 ⊢ 𝐴 ∈ V
3		opeldm.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	opeldm 5932	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝑅 → 𝐴 ∈ dom 𝑅)
5	1, 4	sylbi 217	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2108 Vcvv 3488 ⟨cop 4654 class class class wbr 5166 dom cdm 5700

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-ss 3993 df-nul 4353 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-br 5167 df-dm 5710

This theorem is referenced by: imaindm 6330 funcnv3 6648 opabiota 7004 dffv2 7017 dff13 7292 exse2 7957 reldmtpos 8275 rntpos 8280 dftpos4 8286 tpostpos 8287 fprlem1 8341 wfrlem5OLD 8369 iserd 8789 dmttrcl 9790 ttrclse 9796 frrlem15 9826 dcomex 10516 axdc2lem 10517 dmrecnq 11037 cotr2g 15025 shftfval 15119 geolim2 15919 geomulcvg 15924 geoisum1c 15928 cvgrat 15931 ntrivcvg 15945 eftlub 16157 eflegeo 16169 rpnnen2lem5 16266 imasleval 17601 psdmrn 18643 psssdm2 18651 ovoliunnul 25561 vitalilem5 25666 dvcj 26008 dvrec 26013 dvef 26038 ftc1cn 26104 aaliou3lem3 26404 ulmdv 26464 dvradcnv 26482 abelthlem7 26500 abelthlem9 26502 logtayllem 26719 leibpi 27003 log2tlbnd 27006 zetacvg 27076 hhcms 31235 hhsscms 31310 occl 31336 gsummpt2co 33031 iprodgam 35704 imageval 35894 knoppcnlem6 36464 knoppndvlem6 36483 knoppf 36501 unccur 37563 ftc1cnnc 37652 geomcau 37719 dvradcnv2 44316