Theorem releldm 5955

Description: The first argument of a binary relation belongs to its domain. Note that 𝐴𝑅𝐵 does not imply Rel 𝑅: see for example nrelv 5810 and brv 5477. (Contributed by NM, 2-Jul-2008.)

Assertion

Ref	Expression
releldm	⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex1 5738	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5739	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 484	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5920	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3480   class class class wbr 5143  dom cdm 5685  Rel wrel 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-dm 5695

This theorem is referenced by:  releldmb  5957  releldmi  5959  sofld  6207  funeu  6591  fnbr  6676  funbrfv2b  6966  funfvbrb  7071  ercl  8756  inviso1  17810  setciso  18136  rngciso  20638  ringciso  20672  lmle  25335  dvidlem  25950  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  ulmcau  26438  ulmdvlem3  26445  metideq  33892  heibor1lem  37816  rrncmslem  37839  eqvrelcl  38613  ntrclsiex  44066  ntrneiiex  44089  binomcxplemnn0  44368  binomcxplemnotnn0  44375  sumnnodd  45645  climlimsup  45775  climlimsupcex  45784  climliminflimsupd  45816  liminflimsupclim  45822  dmclimxlim  45866  xlimclimdm  45869  xlimresdm  45874  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  funbrafv  47170  funbrafv2b  47171  rngcisoALTV  48193  ringcisoALTV  48227