Theorem breldm 5777

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3494  ⟨cop 4573   class class class wbr 5066  dom cdm 5555

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-dm 5565

This theorem is referenced by:  funcnv3  6424  opabiota  6746  dffv2  6756  dff13  7013  exse2  7622  reldmtpos  7900  rntpos  7905  dftpos4  7911  tpostpos  7912  wfrlem5  7959  iserd  8315  dcomex  9869  axdc2lem  9870  axdclem2  9942  dmrecnq  10390  cotr2g  14336  shftfval  14429  geolim2  15227  geomulcvg  15232  geoisum1c  15236  cvgrat  15239  ntrivcvg  15253  eftlub  15462  eflegeo  15474  rpnnen2lem5  15571  imasleval  16814  psdmrn  17817  psssdm2  17825  ovoliunnul  24108  vitalilem5  24213  dvcj  24547  dvrec  24552  dvef  24577  ftc1cn  24640  aaliou3lem3  24933  ulmdv  24991  dvradcnv  25009  abelthlem7  25026  abelthlem9  25028  logtayllem  25242  leibpi  25520  log2tlbnd  25523  zetacvg  25592  hhcms  28980  hhsscms  29055  occl  29081  gsummpt2co  30686  iprodgam  32974  imaindm  33022  fprlem1  33137  frrlem15  33142  imageval  33391  knoppcnlem6  33837  knoppndvlem6  33856  knoppf  33874  unccur  34890  ftc1cnnc  34981  geomcau  35049  dvradcnv2  40699