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

Theorem breldmg 5908
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 5151 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑅𝑥𝐴𝑅𝐵))
21spcegv 3586 . . . 4 (𝐵𝐷 → (𝐴𝑅𝐵 → ∃𝑥 𝐴𝑅𝑥))
32imp 405 . . 3 ((𝐵𝐷𝐴𝑅𝐵) → ∃𝑥 𝐴𝑅𝑥)
4 eldmg 5897 . . 3 (𝐴𝐶 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
53, 4imbitrrid 245 . 2 (𝐴𝐶 → ((𝐵𝐷𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅))
653impib 1114 1 ((𝐴𝐶𝐵𝐷𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1085  wex 1779  wcel 2104   class class class wbr 5147  dom cdm 5675
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-dm 5685
This theorem is referenced by:  breldmd  5911  brelrng  5939  releldm  5942  sossfld  6184  brtpos  8222  fprresex  8297  wfrlem17OLD  8327  tfrlem9a  8388  perpln1  28228  lmdvg  33231  esumcvgsum  33384  climeldmeq  44679  climfv  44705  climxlim2  44860  sge0isum  45441  smflimsuplem6  45839  eubrdm  46044  funressneu  46055  tz6.12-afv  46179  rlimdmafv  46183  tz6.12-afv2  46246  rlimdmafv2  46264
  Copyright terms: Public domain W3C validator