Theorem releldm 5924

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

Assertion

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

Proof of Theorem releldm

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3459   class class class wbr 5119  dom cdm 5654  Rel wrel 5659

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-dm 5664

This theorem is referenced by:  releldmb  5926  releldmi  5928  sofld  6176  funeu  6561  fnbr  6646  funbrfv2b  6936  funfvbrb  7041  ercl  8730  inviso1  17779  setciso  18104  rngciso  20598  ringciso  20632  lmle  25253  dvidlem  25868  dvmulbr  25893  dvmulbrOLD  25894  dvcobr  25901  dvcobrOLD  25902  ulmcau  26356  ulmdvlem3  26363  metideq  33924  heibor1lem  37833  rrncmslem  37856  eqvrelcl  38630  ntrclsiex  44077  ntrneiiex  44100  binomcxplemnn0  44373  binomcxplemnotnn0  44380  sumnnodd  45659  climlimsup  45789  climlimsupcex  45798  climliminflimsupd  45830  liminflimsupclim  45836  dmclimxlim  45880  xlimclimdm  45883  xlimresdm  45888  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  funbrafv  47187  funbrafv2b  47188  rngcisoALTV  48252  ringcisoALTV  48286  isinito3  49385