Theorem breldm 5889

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450  ⟨cop 4589   class class class wbr 5102  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-dm 5660

This theorem is used by:  imaindm  6302  funcnv3  6610  opabiota  6967  dffv2  6980  dff13  7258  exse2  7929  reldmtpos  8251  rntpos  8256  dftpos4  8262  tpostpos  8263  fprlem1  8318  iserd  8744  dmttrcl  9722  ttrclse  9728  frrlem15  9761  dcomex  10525  axdc2lem  10526  dmrecnq  11053  cotr2g  15129  shftfval  15223  geolim2  16040  geomulcvg  16045  geoisum1c  16049  cvgrat  16052  ntrivcvg  16066  eftlub  16277  eflegeo  16289  rpnnen2lem5  16386  imasleval  17713  psdmrn  18747  psssdm2  18755  ovoliunnul  25828  vitalilem5  25933  dvcj  26270  dvrec  26275  dvef  26300  ftc1cn  26363  aaliou3lem3  26671  ulmdv  26730  dvradcnv  26748  abelthlem7  26765  abelthlem9  26767  logtayllem  26987  leibpi  27270  log2tlbnd  27273  zetacvg  27342  hhcms  31805  hhsscms  31880  occl  31906  gsummpt2co  33651  iprodgam  36549  imageval  36734  knoppcnlem6  37406  knoppndvlem6  37425  knoppf  37443  unccur  38569  ftc1cnnc  38653  geomcau  38736  dvradcnv2  45373  cocanss2  45964  xpco2  50009