Theorem breldm 5887

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450  ⟨cop 4590   class class class wbr 5103  dom cdm 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5658

This theorem is used by:  imaindm  6292  funcnv3  6599  opabiota  6956  dffv2  6969  dff13  7247  exse2  7913  reldmtpos  8230  rntpos  8235  dftpos4  8241  tpostpos  8242  fprlem1  8297  iserd  8723  dmttrcl  9700  ttrclse  9706  frrlem15  9739  dcomex  10482  axdc2lem  10483  dmrecnq  11010  cotr2g  15082  shftfval  15176  geolim2  15993  geomulcvg  15998  geoisum1c  16002  cvgrat  16005  ntrivcvg  16019  eftlub  16230  eflegeo  16242  rpnnen2lem5  16339  imasleval  17660  psdmrn  18694  psssdm2  18702  ovoliunnul  25775  vitalilem5  25880  dvcj  26217  dvrec  26222  dvef  26247  ftc1cn  26310  aaliou3lem3  26620  ulmdv  26679  dvradcnv  26697  abelthlem7  26714  abelthlem9  26716  logtayllem  26936  leibpi  27219  log2tlbnd  27222  zetacvg  27291  hhcms  31724  hhsscms  31799  occl  31825  gsummpt2co  33528  iprodgam  36422  imageval  36608  knoppcnlem6  37280  knoppndvlem6  37299  knoppf  37317  unccur  38440  ftc1cnnc  38524  geomcau  38607  dvradcnv2  45269  xpco2  49883