Theorem releldm 5886

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

Assertion

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

Proof of Theorem releldm

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3436   class class class wbr 5092  dom cdm 5619  Rel wrel 5624

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 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-rel 5626  df-dm 5629

This theorem is referenced by:  releldmb  5888  releldmi  5890  sofld  6136  funeu  6507  fnbr  6590  funbrfv2b  6880  funfvbrb  6985  ercl  8636  inviso1  17673  setciso  17998  rngciso  20523  ringciso  20557  lmle  25199  dvidlem  25814  dvmulbr  25839  dvmulbrOLD  25840  dvcobr  25847  dvcobrOLD  25848  ulmcau  26302  ulmdvlem3  26309  metideq  33860  heibor1lem  37789  rrncmslem  37812  eqvrelcl  38589  ntrclsiex  44026  ntrneiiex  44049  binomcxplemnn0  44322  binomcxplemnotnn0  44329  sumnnodd  45611  climlimsup  45741  climlimsupcex  45750  climliminflimsupd  45782  liminflimsupclim  45788  dmclimxlim  45832  xlimclimdm  45835  xlimresdm  45840  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  funbrafv  47142  funbrafv2b  47143  rngcisoALTV  48261  ringcisoALTV  48295  isinito3  49485