Theorem releldm 5934

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

Assertion

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

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex1 5714	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5715	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 489	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5899	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  Vcvv 3455   class class class wbr 5109  dom cdm 5661  Rel wrel 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-dm 5671

This theorem is referenced by:  releldmb  5936  releldmi  5938  sofld  6185  funeu  6561  fnbr  6643  funbrfv2b  6938  funfvbrb  7046  ercl  8702  inviso1  17818  setciso  18143  rngciso  20737  ringciso  20771  lmle  25460  dvidlem  26074  dvmulbr  26098  dvcobr  26105  ulmcau  26558  ulmdvlem3  26565  metideq  34283  heibor1lem  38460  rrncmslem  38483  eqvrelcl  39345  ntrclsiex  44779  ntrneiiex  44802  binomcxplemnn0  45059  binomcxplemnotnn0  45066  sumnnodd  46346  climlimsup  46474  climlimsupcex  46483  climliminflimsupd  46515  liminflimsupclim  46521  dmclimxlim  46565  xlimclimdm  46568  xlimresdm  46573  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  funbrafv  47895  funbrafv2b  47896  rngcisoALTV  49042  ringcisoALTV  49076  isinito3  50278