Theorem releldm 5911

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

Assertion

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

Proof of Theorem releldm

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3450   class class class wbr 5110  dom cdm 5641  Rel wrel 5646

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-dm 5651

This theorem is referenced by:  releldmb  5913  releldmi  5915  sofld  6163  funeu  6544  fnbr  6629  funbrfv2b  6921  funfvbrb  7026  ercl  8685  inviso1  17735  setciso  18060  rngciso  20554  ringciso  20588  lmle  25208  dvidlem  25823  dvmulbr  25848  dvmulbrOLD  25849  dvcobr  25856  dvcobrOLD  25857  ulmcau  26311  ulmdvlem3  26318  metideq  33890  heibor1lem  37810  rrncmslem  37833  eqvrelcl  38610  ntrclsiex  44049  ntrneiiex  44072  binomcxplemnn0  44345  binomcxplemnotnn0  44352  sumnnodd  45635  climlimsup  45765  climlimsupcex  45774  climliminflimsupd  45806  liminflimsupclim  45812  dmclimxlim  45856  xlimclimdm  45859  xlimresdm  45864  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  funbrafv  47163  funbrafv2b  47164  rngcisoALTV  48269  ringcisoALTV  48303  isinito3  49493