Theorem releldm 5879

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

Assertion

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

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex1 5664	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5665	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 484	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5844	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  Vcvv 3436   class class class wbr 5086  dom cdm 5611  Rel wrel 5616

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-xp 5617  df-rel 5618  df-dm 5621

This theorem is referenced by:  releldmb  5881  releldmi  5883  sofld  6129  funeu  6501  fnbr  6584  funbrfv2b  6874  funfvbrb  6979  ercl  8628  inviso1  17668  setciso  17993  rngciso  20548  ringciso  20582  lmle  25223  dvidlem  25838  dvmulbr  25863  dvmulbrOLD  25864  dvcobr  25871  dvcobrOLD  25872  ulmcau  26326  ulmdvlem3  26333  metideq  33898  heibor1lem  37849  rrncmslem  37872  eqvrelcl  38649  ntrclsiex  44086  ntrneiiex  44109  binomcxplemnn0  44382  binomcxplemnotnn0  44389  sumnnodd  45670  climlimsup  45798  climlimsupcex  45807  climliminflimsupd  45839  liminflimsupclim  45845  dmclimxlim  45889  xlimclimdm  45892  xlimresdm  45897  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  funbrafv  47189  funbrafv2b  47190  rngcisoALTV  48308  ringcisoALTV  48342  isinito3  49532