Theorem releldm 5942

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

Assertion

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

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex1 5728	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5729	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 483	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5908	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1369	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  Vcvv 3472   class class class wbr 5147  dom cdm 5675  Rel wrel 5680

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-dm 5685

This theorem is referenced by:  releldmb  5944  releldmi  5946  sofld  6185  funeu  6572  fnbr  6656  funbrfv2b  6948  funfvbrb  7051  ercl  8716  inviso1  17717  setciso  18045  lmle  25049  dvidlem  25664  dvmulbr  25689  dvmulbrOLD  25690  dvcobr  25697  dvcobrOLD  25698  ulmcau  26143  ulmdvlem3  26150  metideq  33171  heibor1lem  36980  rrncmslem  37003  eqvrelcl  37785  ntrclsiex  43106  ntrneiiex  43129  binomcxplemnn0  43410  binomcxplemnotnn0  43417  sumnnodd  44644  climlimsup  44774  climlimsupcex  44783  climliminflimsupd  44815  liminflimsupclim  44821  dmclimxlim  44865  xlimclimdm  44868  xlimresdm  44873  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  funbrafv  46164  funbrafv2b  46165  rngciso  46968  rngcisoALTV  46980  ringciso  47019  ringcisoALTV  47043