Theorem breldm 5329

Description: Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)

Hypotheses

Ref	Expression
opeldm.1	|- A e. _V
opeldm.2	|- B e. _V

Assertion

Ref	Expression
breldm	|- ( A R B -> A e. dom R )

Proof of Theorem breldm

Step	Hyp	Ref	Expression
1		df-br 4654	. 2 |- ( A R B <-> <. A , B >. e. R )
2		opeldm.1	. . 3 |- A e. _V
3		opeldm.2	. . 3 |- B e. _V
4	2, 3	opeldm 5328	. 2 |- ( <. A , B >. e. R -> A e. dom R )
5	1, 4	sylbi 207	1 |- ( A R B -> A e. dom R )

Syntax hints:   -> wi 4   e. wcel 1990   _Vcvv 3200   <.cop 4183   class class class wbr 4653   dom cdm 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-dm 5124

This theorem is referenced by:  funcnv3  5959  opabiota  6261  dffv2  6271  dff13  6512  exse2  7105  reldmtpos  7360  rntpos  7365  dftpos4  7371  tpostpos  7372  wfrlem5  7419  iserd  7768  dcomex  9269  axdc2lem  9270  axdclem2  9342  dmrecnq  9790  cotr2g  13715  shftfval  13810  geolim2  14602  geomulcvg  14607  geoisum1c  14611  cvgrat  14615  ntrivcvg  14629  eftlub  14839  eflegeo  14851  rpnnen2lem5  14947  imasleval  16201  psdmrn  17207  psssdm2  17215  ovoliunnul  23275  vitalilem5  23381  dvcj  23713  dvrec  23718  dvef  23743  ftc1cn  23806  aaliou3lem3  24099  ulmdv  24157  dvradcnv  24175  abelthlem7  24192  abelthlem9  24194  logtayllem  24405  leibpi  24669  log2tlbnd  24672  zetacvg  24741  hhcms  28060  hhsscms  28136  occl  28163  gsummpt2co  29780  iprodgam  31628  imaindm  31682  frrlem5  31784  imageval  32037  knoppcnlem6  32488  knoppndvlem6  32508  knoppf  32526  unccur  33392  ftc1cnnc  33484  geomcau  33555  dvradcnv2  38546