Theorem releldm 5654

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

Assertion

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

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex1 5451	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5452	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 477	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5624	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1351	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2050  Vcvv 3409   class class class wbr 4925  dom cdm 5403  Rel wrel 5408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744  ax-sep 5056  ax-nul 5063  ax-pr 5182

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4926  df-opab 4988  df-xp 5409  df-rel 5410  df-dm 5413

This theorem is referenced by:  releldmb  5656  releldmi  5658  sofld  5881  funeu  6210  fnbr  6289  funbrfv2b  6550  funfvbrb  6644  ercl  8098  inviso1  16906  setciso  17221  lmle  23619  dvidlem  24228  dvmulbr  24251  dvcobr  24258  ulmcau  24698  ulmdvlem3  24705  metideq  30806  heibor1lem  34558  rrncmslem  34581  eqvrelcl  35321  ntrclsiex  39795  ntrneiiex  39818  binomcxplemnn0  40126  binomcxplemnotnn0  40133  sumnnodd  41367  climlimsup  41497  climlimsupcex  41506  climliminflimsupd  41538  liminflimsupclim  41544  dmclimxlim  41588  xlimclimdm  41591  xlimresdm  41596  ioodvbdlimc1lem2  41672  ioodvbdlimc2lem  41674  funbrafv  42788  funbrafv2b  42789  rngciso  43642  rngcisoALTV  43654  ringciso  43693  ringcisoALTV  43717