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

Theorem eldm2 5763
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 5761 . 2 (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wex 1771  wcel 2105  Vcvv 3492  cop 4563  dom cdm 5548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-dm 5558
This theorem is referenced by:  dmss  5764  opeldm  5769  dmin  5773  dmiun  5775  dmuni  5776  dm0  5783  reldm0  5791  dmrnssfld  5834  dmcoss  5835  dmcosseq  5837  dmres  5868  iss  5896  dmsnopg  6063  relssdmrn  6114  funssres  6391  dmfco  6750  fiun  7633  f1iun  7634  wfrlem12  7955  axdc3lem2  9861  fnpr2ob  16819  gsum2d2  19023  cnlnssadj  29784  prsdm  31056  eldm3  32894  dfdm5  32913  frrlem8  33027  frrlem10  33029  iss2  35482
  Copyright terms: Public domain W3C validator