Theorem releldm 5957

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

Assertion

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

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex1 5741	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5742	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 484	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5922	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1370	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  Vcvv 3477   class class class wbr 5147  dom cdm 5688  Rel wrel 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-dm 5698

This theorem is referenced by:  releldmb  5959  releldmi  5961  sofld  6208  funeu  6592  fnbr  6676  funbrfv2b  6965  funfvbrb  7070  ercl  8754  inviso1  17813  setciso  18144  rngciso  20654  ringciso  20688  lmle  25348  dvidlem  25964  dvmulbr  25989  dvmulbrOLD  25990  dvcobr  25997  dvcobrOLD  25998  ulmcau  26452  ulmdvlem3  26459  metideq  33853  heibor1lem  37795  rrncmslem  37818  eqvrelcl  38593  ntrclsiex  44042  ntrneiiex  44065  binomcxplemnn0  44344  binomcxplemnotnn0  44351  sumnnodd  45585  climlimsup  45715  climlimsupcex  45724  climliminflimsupd  45756  liminflimsupclim  45762  dmclimxlim  45806  xlimclimdm  45809  xlimresdm  45814  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  funbrafv  47107  funbrafv2b  47108  rngcisoALTV  48120  ringcisoALTV  48154