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 5412. (Contributed by NM, 2-Jul-2008.)

Assertion

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

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex1 5671	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5672	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 485	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5851	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1379	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  Vcvv 3431   class class class wbr 5072  dom cdm 5618  Rel wrel 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-dm 5628

This theorem is referenced by:  releldmb  5888  releldmi  5890  sofld  6138  funeu  6510  fnbr  6593  funbrfv2b  6884  funfvbrb  6992  ercl  8645  inviso1  17724  setciso  18049  rngciso  20610  ringciso  20644  lmle  25286  dvidlem  25900  dvmulbr  25924  dvcobr  25931  ulmcau  26378  ulmdvlem3  26385  metideq  34077  heibor1lem  38176  rrncmslem  38199  eqvrelcl  39063  ntrclsiex  44497  ntrneiiex  44520  binomcxplemnn0  44793  binomcxplemnotnn0  44800  sumnnodd  46075  climlimsup  46203  climlimsupcex  46212  climliminflimsupd  46244  liminflimsupclim  46250  dmclimxlim  46294  xlimclimdm  46297  xlimresdm  46302  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  funbrafv  47621  funbrafv2b  47622  rngcisoALTV  48768  ringcisoALTV  48802  isinito3  49990