Theorem releldm 5894

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

Assertion

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

Proof of Theorem releldm

Step	Hyp	Ref	Expression
1		brrelex1 5678	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
2		brrelex2 5679	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
3		simpr 484	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4		breldmg 5859	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
5	1, 2, 3, 4	syl3anc 1374	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3430   class class class wbr 5086  dom cdm 5625  Rel wrel 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5631  df-rel 5632  df-dm 5635

This theorem is referenced by:  releldmb  5896  releldmi  5898  sofld  6146  funeu  6518  fnbr  6601  funbrfv2b  6892  funfvbrb  6998  ercl  8649  inviso1  17727  setciso  18052  rngciso  20609  ringciso  20643  lmle  25281  dvidlem  25895  dvmulbr  25919  dvcobr  25926  ulmcau  26376  ulmdvlem3  26383  metideq  34056  heibor1lem  38147  rrncmslem  38170  eqvrelcl  39034  ntrclsiex  44501  ntrneiiex  44524  binomcxplemnn0  44797  binomcxplemnotnn0  44804  sumnnodd  46081  climlimsup  46209  climlimsupcex  46218  climliminflimsupd  46250  liminflimsupclim  46256  dmclimxlim  46300  xlimclimdm  46303  xlimresdm  46308  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  funbrafv  47621  funbrafv2b  47622  rngcisoALTV  48768  ringcisoALTV  48802  isinito3  49990