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

Theorem eldm 5911
Description: Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
Hypothesis
Ref Expression
eldm.1 𝐴 ∈ V
Assertion
Ref Expression
eldm (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵

Proof of Theorem eldm
StepHypRef Expression
1 eldm.1 . 2 𝐴 ∈ V
2 eldmg 5909 . 2 (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
31, 2ax-mp 5 1 (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wex 1779  wcel 2108  Vcvv 3480   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:  dmi  5932  dmep  5934  dmxp  5939  dmcoss  5985  dmcosseq  5987  dmcosseqOLD  5988  dminss  6173  dmsnn0  6227  dffun7  6593  dffun8  6594  fnres  6695  opabiota  6991  fndmdif  7062  dff3  7120  frxp  8151  suppvalbr  8189  reldmtpos  8259  dmtpos  8263  aceq3lem  10160  axdc2lem  10488  axdclem2  10560  fpwwe2lem11  10681  nqerf  10970  shftdm  15110  bcthlem4  25361  dchrisumlem3  27535  eulerpath  30260  fundmpss  35767  elfix  35904  fnsingle  35920  fnimage  35930  funpartlem  35943  dfrecs2  35951  dfrdg4  35952  knoppcnlem9  36502  prtlem16  38870  undmrnresiss  43617
  Copyright terms: Public domain W3C validator