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 5906

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2106 Vcvv 3474 ⟨cop 4633 class class class wbr 5147 dom cdm 5675

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-dm 5685

This theorem is referenced by: imaindm 6295 funcnv3 6615 opabiota 6971 dffv2 6983 dff13 7250 exse2 7904 reldmtpos 8215 rntpos 8220 dftpos4 8226 tpostpos 8227 fprlem1 8281 wfrlem5OLD 8309 iserd 8725 dmttrcl 9712 ttrclse 9718 frrlem15 9748 dcomex 10438 axdc2lem 10439 dmrecnq 10959 cotr2g 14919 shftfval 15013 geolim2 15813 geomulcvg 15818 geoisum1c 15822 cvgrat 15825 ntrivcvg 15839 eftlub 16048 eflegeo 16060 rpnnen2lem5 16157 imasleval 17483 psdmrn 18522 psssdm2 18530 ovoliunnul 25015 vitalilem5 25120 dvcj 25458 dvrec 25463 dvef 25488 ftc1cn 25551 aaliou3lem3 25848 ulmdv 25906 dvradcnv 25924 abelthlem7 25941 abelthlem9 25943 logtayllem 26158 leibpi 26436 log2tlbnd 26439 zetacvg 26508 hhcms 30443 hhsscms 30518 occl 30544 gsummpt2co 32187 iprodgam 34700 imageval 34890 knoppcnlem6 35362 knoppndvlem6 35381 knoppf 35399 unccur 36459 ftc1cnnc 36548 geomcau 36615 dvradcnv2 43091