Theorem breldm 5820

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3433  ⟨cop 4568   class class class wbr 5075  dom cdm 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-dm 5600

This theorem is referenced by:  funcnv3  6511  opabiota  6860  dffv2  6872  dff13  7137  exse2  7773  reldmtpos  8059  rntpos  8064  dftpos4  8070  tpostpos  8071  fprlem1  8125  wfrlem5OLD  8153  iserd  8533  dmttrcl  9488  ttrclse  9494  frrlem15  9524  dcomex  10212  axdc2lem  10213  dmrecnq  10733  cotr2g  14696  shftfval  14790  geolim2  15592  geomulcvg  15597  geoisum1c  15601  cvgrat  15604  ntrivcvg  15618  eftlub  15827  eflegeo  15839  rpnnen2lem5  15936  imasleval  17261  psdmrn  18300  psssdm2  18308  ovoliunnul  24680  vitalilem5  24785  dvcj  25123  dvrec  25128  dvef  25153  ftc1cn  25216  aaliou3lem3  25513  ulmdv  25571  dvradcnv  25589  abelthlem7  25606  abelthlem9  25608  logtayllem  25823  leibpi  26101  log2tlbnd  26104  zetacvg  26173  hhcms  29574  hhsscms  29649  occl  29675  gsummpt2co  31317  iprodgam  33717  imaindm  33762  imageval  34241  knoppcnlem6  34687  knoppndvlem6  34706  knoppf  34724  unccur  35769  ftc1cnnc  35858  geomcau  35926  dvradcnv2  41972