Theorem releldm 5891

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

Assertion

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

Proof of Theorem releldm

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3438   class class class wbr 5096  dom cdm 5622  Rel wrel 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-rel 5629  df-dm 5632

This theorem is referenced by:  releldmb  5893  releldmi  5895  sofld  6143  funeu  6515  fnbr  6598  funbrfv2b  6889  funfvbrb  6994  ercl  8644  inviso1  17688  setciso  18013  rngciso  20569  ringciso  20603  lmle  25255  dvidlem  25870  dvmulbr  25895  dvmulbrOLD  25896  dvcobr  25903  dvcobrOLD  25904  ulmcau  26358  ulmdvlem3  26365  metideq  33999  heibor1lem  37949  rrncmslem  37972  eqvrelcl  38808  ntrclsiex  44236  ntrneiiex  44259  binomcxplemnn0  44532  binomcxplemnotnn0  44539  sumnnodd  45818  climlimsup  45946  climlimsupcex  45955  climliminflimsupd  45987  liminflimsupclim  45993  dmclimxlim  46037  xlimclimdm  46040  xlimresdm  46045  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  funbrafv  47346  funbrafv2b  47347  rngcisoALTV  48465  ringcisoALTV  48499  isinito3  49687