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

Theorem breldmg 5920
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 5147 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑅𝑥𝐴𝑅𝐵))
21spcegv 3597 . . . 4 (𝐵𝐷 → (𝐴𝑅𝐵 → ∃𝑥 𝐴𝑅𝑥))
32imp 406 . . 3 ((𝐵𝐷𝐴𝑅𝐵) → ∃𝑥 𝐴𝑅𝑥)
4 eldmg 5909 . . 3 (𝐴𝐶 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
53, 4imbitrrid 246 . 2 (𝐴𝐶 → ((𝐵𝐷𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅))
653impib 1117 1 ((𝐴𝐶𝐵𝐷𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087  wex 1779  wcel 2108   class class class wbr 5143  dom cdm 5685
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-dm 5695
This theorem is referenced by:  breldmd  5923  brelrng  5952  releldm  5955  sossfld  6206  brtpos  8260  fprresex  8335  wfrlem17OLD  8365  tfrlem9a  8426  perpln1  28718  lmdvg  33952  esumcvgsum  34089  climeldmeq  45680  climfv  45706  climxlim2  45861  sge0isum  46442  smflimsuplem6  46840  eubrdm  47048  funressneu  47059  tz6.12-afv  47185  rlimdmafv  47189  tz6.12-afv2  47252  rlimdmafv2  47270
  Copyright terms: Public domain W3C validator