Theorem releldmi 5912

Description: The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.)

Hypothesis

Ref	Expression
releldm.1	⊢ Rel 𝑅

Assertion

Ref	Expression
releldmi	⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

Proof of Theorem releldmi

Step	Hyp	Ref	Expression
1		releldm.1	. 2 ⊢ Rel 𝑅
2		releldm 5908	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
3	1, 2	mpan 690	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5107  dom cdm 5638  Rel wrel 5643

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-dm 5648

This theorem is referenced by:  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2lem12  10595  rlimpm  15466  rlimdm  15517  iserex  15623  caucvgrlem2  15641  caucvgr  15642  caurcvg2  15644  caucvg  15645  fsumcvg3  15695  cvgcmpce  15784  climcnds  15817  trirecip  15829  ledm  18549  cmetcaulem  25188  ovoliunlem1  25403  mbflimlem  25568  dvaddf  25845  dvmulf  25846  dvcof  25852  dvcnv  25881  abelthlem5  26345  emcllem6  26911  lgamgulmlem4  26942  hlimcaui  31165  brfvrcld2  43681  sumnnodd  45628  climliminf  45804  stirlinglem12  46083  fouriersw  46229  rlimdmafv  47178  rlimdmafv2  47259