Theorem breldm 5779

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3496  ⟨cop 4575   class class class wbr 5068  dom cdm 5557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-dm 5567

This theorem is referenced by:  funcnv3  6426  opabiota  6748  dffv2  6758  dff13  7015  exse2  7624  reldmtpos  7902  rntpos  7907  dftpos4  7913  tpostpos  7914  wfrlem5  7961  iserd  8317  dcomex  9871  axdc2lem  9872  axdclem2  9944  dmrecnq  10392  cotr2g  14338  shftfval  14431  geolim2  15229  geomulcvg  15234  geoisum1c  15238  cvgrat  15241  ntrivcvg  15255  eftlub  15464  eflegeo  15476  rpnnen2lem5  15573  imasleval  16816  psdmrn  17819  psssdm2  17827  ovoliunnul  24110  vitalilem5  24215  dvcj  24549  dvrec  24554  dvef  24579  ftc1cn  24642  aaliou3lem3  24935  ulmdv  24993  dvradcnv  25011  abelthlem7  25028  abelthlem9  25030  logtayllem  25244  leibpi  25522  log2tlbnd  25525  zetacvg  25594  hhcms  28982  hhsscms  29057  occl  29083  gsummpt2co  30688  iprodgam  32976  imaindm  33024  fprlem1  33139  frrlem15  33144  imageval  33393  knoppcnlem6  33839  knoppndvlem6  33858  knoppf  33876  unccur  34877  ftc1cnnc  34968  geomcau  35036  dvradcnv2  40686