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

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

Proof of Theorem eldm2
StepHypRef Expression
1 eldm.1 . 2 𝐴 ∈ V
2 eldm2g 5900 . 2 (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wex 1782  wcel 2107  Vcvv 3475  cop 4635  dom cdm 5677
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 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-dm 5687
This theorem is referenced by:  dmss  5903  opeldm  5908  dmin  5912  dmiun  5914  dmuni  5915  dm0  5921  reldm0  5928  dmrnssfld  5970  dmcoss  5971  dmcosseq  5973  dmres  6004  iss  6036  dmsnopg  6213  relssdmrnOLD  6269  funssres  6593  dmfco  6988  fiun  7929  f1iun  7930  frrlem8  8278  frrlem10  8280  wfrlem12OLD  8320  axdc3lem2  10446  fnpr2ob  17504  gsum2d2  19842  cnlnssadj  31333  prsdm  32894  eldm3  34731  dfdm5  34744  iss2  37213
  Copyright terms: Public domain W3C validator