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 5919

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2108 Vcvv 3480 ⟨cop 4632 class class class wbr 5143 dom cdm 5685

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

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-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-dm 5695

This theorem is referenced by: imaindm 6319 funcnv3 6636 opabiota 6991 dffv2 7004 dff13 7275 exse2 7939 reldmtpos 8259 rntpos 8264 dftpos4 8270 tpostpos 8271 fprlem1 8325 wfrlem5OLD 8353 iserd 8771 dmttrcl 9761 ttrclse 9767 frrlem15 9797 dcomex 10487 axdc2lem 10488 dmrecnq 11008 cotr2g 15015 shftfval 15109 geolim2 15907 geomulcvg 15912 geoisum1c 15916 cvgrat 15919 ntrivcvg 15933 eftlub 16145 eflegeo 16157 rpnnen2lem5 16254 imasleval 17586 psdmrn 18618 psssdm2 18626 ovoliunnul 25542 vitalilem5 25647 dvcj 25988 dvrec 25993 dvef 26018 ftc1cn 26084 aaliou3lem3 26386 ulmdv 26446 dvradcnv 26464 abelthlem7 26482 abelthlem9 26484 logtayllem 26701 leibpi 26985 log2tlbnd 26988 zetacvg 27058 hhcms 31222 hhsscms 31297 occl 31323 gsummpt2co 33051 iprodgam 35742 imageval 35931 knoppcnlem6 36499 knoppndvlem6 36518 knoppf 36536 unccur 37610 ftc1cnnc 37699 geomcau 37766 dvradcnv2 44366