Theorem releldm 5814

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

Assertion

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

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex1 5605	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5606	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 487	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5778	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1367	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  Vcvv 3494   class class class wbr 5066  dom cdm 5555  Rel wrel 5560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-rel 5562  df-dm 5565

This theorem is referenced by:  releldmb  5816  releldmi  5818  sofld  6044  funeu  6380  fnbr  6459  funbrfv2b  6723  funfvbrb  6821  ercl  8300  inviso1  17036  setciso  17351  lmle  23904  dvidlem  24513  dvmulbr  24536  dvcobr  24543  ulmcau  24983  ulmdvlem3  24990  metideq  31133  heibor1lem  35102  rrncmslem  35125  eqvrelcl  35862  ntrclsiex  40423  ntrneiiex  40446  binomcxplemnn0  40701  binomcxplemnotnn0  40708  sumnnodd  41931  climlimsup  42061  climlimsupcex  42070  climliminflimsupd  42102  liminflimsupclim  42108  dmclimxlim  42152  xlimclimdm  42155  xlimresdm  42160  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  funbrafv  43377  funbrafv2b  43378  rngciso  44273  rngcisoALTV  44285  ringciso  44324  ringcisoALTV  44348