Theorem releldm 5853

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

Assertion

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

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex1 5640	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5641	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 485	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5818	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1370	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3432   class class class wbr 5074  dom cdm 5589  Rel wrel 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-dm 5599

This theorem is referenced by:  releldmb  5855  releldmi  5857  sofld  6090  funeu  6459  fnbr  6541  funbrfv2b  6827  funfvbrb  6928  ercl  8509  inviso1  17478  setciso  17806  lmle  24465  dvidlem  25079  dvmulbr  25103  dvcobr  25110  ulmcau  25554  ulmdvlem3  25561  metideq  31843  heibor1lem  35967  rrncmslem  35990  eqvrelcl  36725  ntrclsiex  41663  ntrneiiex  41686  binomcxplemnn0  41967  binomcxplemnotnn0  41974  sumnnodd  43171  climlimsup  43301  climlimsupcex  43310  climliminflimsupd  43342  liminflimsupclim  43348  dmclimxlim  43392  xlimclimdm  43395  xlimresdm  43400  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  funbrafv  44650  funbrafv2b  44651  rngciso  45540  rngcisoALTV  45552  ringciso  45591  ringcisoALTV  45615