Theorem releldm 5148

Description: The first argument of a binary relation belongs to its domain. (Contributed by NM, 2-Jul-2008.)

Assertion

Ref	Expression
releldm	|- ( ( Rel R /\ A R B ) -> A e. dom R )

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex 4952	. 2 |- ( ( Rel R /\ A R B ) -> A e. _V )
2		brrelex2 4953	. 2 |- ( ( Rel R /\ A R B ) -> B e. _V )
3		simpr 459	. 2 |- ( ( Rel R /\ A R B ) -> A R B )
4		breldmg 5121	. 2 |- ( ( A e. _V /\ B e. _V /\ A R B ) -> A e. dom R )
5	1, 2, 3, 4	syl3anc 1226	1 |- ( ( Rel R /\ A R B ) -> A e. dom R )

Syntax hints:   -> wi 4   /\ wa 367   e. wcel 1826   _Vcvv 3034   class class class wbr 4367   dom cdm 4913   Rel wrel 4918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-xp 4919  df-rel 4920  df-dm 4923

This theorem is referenced by:  releldmb  5150  releldmi  5152  sofld  5364  funeu  5520  fnbr  5591  funbrfv2b  5818  funfvbrb  5902  ercl  7240  inviso1  15172  setciso  15487  lmle  21825  dvidlem  22404  dvmulbr  22427  dvcobr  22434  ulmcau  22875  ulmdvlem3  22882  uhgraun  24432  umgraun  24449  metideq  28026  heibor1lem  30471  rrncmslem  30494  binomcxplemnn0  31422  binomcxplemnotnn0  31429  sumnnodd  31802  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  funbrafv  32409  funbrafv2b  32410  rngciso  32990  rngcisoALTV  33002  ringciso  33041  ringcisoALTV  33065