Theorem breldm 5361

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

Syntax hints:   → wi 4   ∈ wcel 2030  Vcvv 3231  ⟨cop 4216   class class class wbr 4685  dom cdm 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-dm 5153

This theorem is referenced by:  funcnv3  5997  opabiota  6300  dffv2  6310  dff13  6552  exse2  7147  reldmtpos  7405  rntpos  7410  dftpos4  7416  tpostpos  7417  wfrlem5  7464  iserd  7813  dcomex  9307  axdc2lem  9308  axdclem2  9380  dmrecnq  9828  cotr2g  13761  shftfval  13854  geolim2  14646  geomulcvg  14651  geoisum1c  14655  cvgrat  14659  ntrivcvg  14673  eftlub  14883  eflegeo  14895  rpnnen2lem5  14991  imasleval  16248  psdmrn  17254  psssdm2  17262  ovoliunnul  23321  vitalilem5  23426  dvcj  23758  dvrec  23763  dvef  23788  ftc1cn  23851  aaliou3lem3  24144  ulmdv  24202  dvradcnv  24220  abelthlem7  24237  abelthlem9  24239  logtayllem  24450  leibpi  24714  log2tlbnd  24717  zetacvg  24786  hhcms  28188  hhsscms  28264  occl  28291  gsummpt2co  29908  iprodgam  31754  imaindm  31806  frrlem5  31909  imageval  32162  knoppcnlem6  32613  knoppndvlem6  32633  knoppf  32651  unccur  33522  ftc1cnnc  33614  geomcau  33685  dvradcnv2  38863