MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  releldm Structured version   Visualization version   GIF version

Theorem releldm 5347
Description: The first argument of a binary relation belongs to its domain. (Contributed by NM, 2-Jul-2008.)
Assertion
Ref Expression
releldm ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Proof of Theorem releldm
StepHypRef Expression
1 brrelex 5146 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ V)
2 brrelex2 5147 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐵 ∈ V)
3 simpr 477 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴𝑅𝐵)
4 breldmg 5319 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
51, 2, 3, 4syl3anc 1324 1 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1988  Vcvv 3195   class class class wbr 4644  dom cdm 5104  Rel wrel 5109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-xp 5110  df-rel 5111  df-dm 5114
This theorem is referenced by:  releldmb  5349  releldmi  5351  sofld  5569  funeu  5901  fnbr  5981  funbrfv2b  6227  funfvbrb  6316  ercl  7738  inviso1  16407  setciso  16722  lmle  23080  dvidlem  23660  dvmulbr  23683  dvcobr  23690  ulmcau  24130  ulmdvlem3  24137  metideq  29910  heibor1lem  33579  rrncmslem  33602  ntrclsiex  38171  ntrneiiex  38194  binomcxplemnn0  38368  binomcxplemnotnn0  38375  sumnnodd  39662  climlimsup  39786  climlimsupcex  39795  climliminflimsupd  39827  liminflimsupclim  39833  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  funbrafv  41001  funbrafv2b  41002  rngciso  41747  rngcisoALTV  41759  ringciso  41798  ringcisoALTV  41822
  Copyright terms: Public domain W3C validator