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 5857

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 5076	. 2 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2		opeldm.1	. . 3 ⊢ 𝐴 ∈ V
3		opeldm.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	opeldm 5856	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝑅 → 𝐴 ∈ dom 𝑅)
5	1, 4	sylbi 219	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2121 Vcvv 3433 ⟨cop 4564 class class class wbr 5075 dom cdm 5621

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 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-ext 2713

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-sb 2075 df-clab 2720 df-cleq 2733 df-clel 2816 df-rab 3394 df-v 3435 df-dif 3888 df-un 3890 df-ss 3902 df-nul 4265 df-if 4458 df-sn 4559 df-pr 4561 df-op 4565 df-br 5076 df-dm 5631

This theorem is referenced by: imaindm 6254 funcnv3 6559 opabiota 6913 dffv2 6926 dff13 7202 exse2 7861 reldmtpos 8178 rntpos 8183 dftpos4 8189 tpostpos 8190 fprlem1 8244 iserd 8664 dmttrcl 9637 ttrclse 9643 frrlem15 9676 dcomex 10364 axdc2lem 10365 dmrecnq 10886 cotr2g 14933 shftfval 15027 geolim2 15831 geomulcvg 15836 geoisum1c 15840 cvgrat 15843 ntrivcvg 15857 eftlub 16071 eflegeo 16083 rpnnen2lem5 16180 imasleval 17500 psdmrn 18534 psssdm2 18542 ovoliunnul 25496 vitalilem5 25601 dvcj 25939 dvrec 25944 dvef 25969 ftc1cn 26032 aaliou3lem3 26332 ulmdv 26390 dvradcnv 26408 abelthlem7 26425 abelthlem9 26427 logtayllem 26645 leibpi 26928 log2tlbnd 26931 zetacvg 27000 hhcms 31296 hhsscms 31371 occl 31397 gsummpt2co 33133 iprodgam 35985 imageval 36171 knoppcnlem6 36819 knoppndvlem6 36838 knoppf 36856 unccur 37985 ftc1cnnc 38074 geomcau 38141 dvradcnv2 44806 xpco2 49361