Theorem releldm 5897

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

Assertion

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

Proof of Theorem releldm

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3444   class class class wbr 5102  dom cdm 5631  Rel wrel 5636

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638  df-dm 5641

This theorem is referenced by:  releldmb  5899  releldmi  5901  sofld  6148  funeu  6525  fnbr  6608  funbrfv2b  6900  funfvbrb  7005  ercl  8659  inviso1  17704  setciso  18029  rngciso  20523  ringciso  20557  lmle  25177  dvidlem  25792  dvmulbr  25817  dvmulbrOLD  25818  dvcobr  25825  dvcobrOLD  25826  ulmcau  26280  ulmdvlem3  26287  metideq  33856  heibor1lem  37776  rrncmslem  37799  eqvrelcl  38576  ntrclsiex  44015  ntrneiiex  44038  binomcxplemnn0  44311  binomcxplemnotnn0  44318  sumnnodd  45601  climlimsup  45731  climlimsupcex  45740  climliminflimsupd  45772  liminflimsupclim  45778  dmclimxlim  45822  xlimclimdm  45825  xlimresdm  45830  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  funbrafv  47132  funbrafv2b  47133  rngcisoALTV  48238  ringcisoALTV  48272  isinito3  49462