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

Theorem eldm 5566
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 5564 . 2 (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
31, 2ax-mp 5 1 (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wex 1823  wcel 2107  Vcvv 3398   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:  dmi  5585  dmcoss  5631  dmcosseq  5633  dminss  5801  dmsnn0  5854  dffun7  6162  dffun8  6163  fnres  6253  opabiota  6521  fndmdif  6584  dff3  6636  frxp  7568  suppvalbr  7580  reldmtpos  7642  dmtpos  7646  aceq3lem  9276  axdc2lem  9605  axdclem2  9677  fpwwe2lem12  9798  nqerf  10087  shftdm  14218  xpsfrnel2  16611  bcthlem4  23533  dchrisumlem3  25632  eulerpath  27645  fundmpss  32257  elfix  32599  fnsingle  32615  fnimage  32625  funpartlem  32638  dfrecs2  32646  dfrdg4  32647  knoppcnlem9  33074  prtlem16  35023  undmrnresiss  38867
  Copyright terms: Public domain W3C validator