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

Theorem breldmg 5746
Description: Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)
Assertion
Ref Expression
breldmg ((𝐴𝐶𝐵𝐷𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Proof of Theorem breldmg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 breq2 5037 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑅𝑥𝐴𝑅𝐵))
21spcegv 3548 . . . 4 (𝐵𝐷 → (𝐴𝑅𝐵 → ∃𝑥 𝐴𝑅𝑥))
32imp 410 . . 3 ((𝐵𝐷𝐴𝑅𝐵) → ∃𝑥 𝐴𝑅𝑥)
4 eldmg 5735 . . 3 (𝐴𝐶 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
53, 4syl5ibr 249 . 2 (𝐴𝐶 → ((𝐵𝐷𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅))
653impib 1113 1 ((𝐴𝐶𝐵𝐷𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084  wex 1781  wcel 2112   class class class wbr 5033  dom cdm 5523
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-un 3889  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-dm 5533
This theorem is referenced by:  breldmd  5749  brelrng  5779  releldm  5782  sossfld  6014  brtpos  7888  wfrlem17  7958  tfrlem9a  8009  perpln1  26508  lmdvg  31310  esumcvgsum  31461  climeldmeq  42304  climfv  42330  climxlim2  42485  sge0isum  43063  smflimsuplem6  43453  eubrdm  43625  funressneu  43636  tz6.12-afv  43726  rlimdmafv  43730  tz6.12-afv2  43793  rlimdmafv2  43811
  Copyright terms: Public domain W3C validator