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

Theorem breldmg 5575
 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 4890 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑅𝑥𝐴𝑅𝐵))
21spcegv 3496 . . . 4 (𝐵𝐷 → (𝐴𝑅𝐵 → ∃𝑥 𝐴𝑅𝑥))
32imp 397 . . 3 ((𝐵𝐷𝐴𝑅𝐵) → ∃𝑥 𝐴𝑅𝑥)
4 eldmg 5564 . . 3 (𝐴𝐶 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
53, 4syl5ibr 238 . 2 (𝐴𝐶 → ((𝐵𝐷𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅))
653impib 1105 1 ((𝐴𝐶𝐵𝐷𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071  ∃wex 1823   ∈ wcel 2107   class class class wbr 4886  dom cdm 5355 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-dm 5365 This theorem is referenced by:  brelrng  5601  releldm  5604  sossfld  5834  brtpos  7643  wfrlem17  7714  tfrlem9a  7765  perpln1  26061  lmdvg  30597  esumcvgsum  30748  breldmd  40273  fvelimad  40375  climeldmeq  40809  climfv  40835  climxlim2  40990  sge0isum  41572  smflimsuplem6  41962  eubrdm  42104  funressneu  42116  tz6.12-afv  42218  rlimdmafv  42222  tz6.12-afv2  42285  rlimdmafv2  42303
 Copyright terms: Public domain W3C validator