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

Theorem eldm 5857
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 5855 . 2 (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
31, 2ax-mp 5 1 (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wex 1782  wcel 2107  Vcvv 3444   class class class wbr 5106  dom cdm 5634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-dm 5644
This theorem is referenced by:  dmi  5878  dmep  5880  dmcoss  5927  dmcosseq  5929  dminss  6106  dmsnn0  6160  dffun7  6529  dffun8  6530  fnres  6629  opabiota  6925  fndmdif  6993  dff3  7051  frxp  8059  suppvalbr  8097  reldmtpos  8166  dmtpos  8170  aceq3lem  10061  axdc2lem  10389  axdclem2  10461  fpwwe2lem11  10582  nqerf  10871  shftdm  14962  bcthlem4  24707  dchrisumlem3  26855  eulerpath  29227  fundmpss  34397  elfix  34534  fnsingle  34550  fnimage  34560  funpartlem  34573  dfrecs2  34581  dfrdg4  34582  knoppcnlem9  35010  prtlem16  37377  undmrnresiss  41964
  Copyright terms: Public domain W3C validator