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

Theorem eldm2 5914
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 5912 . 2 (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wex 1775  wcel 2105  Vcvv 3477  cop 4636  dom cdm 5688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-dm 5698
This theorem is referenced by:  dmss  5915  opeldm  5920  dmin  5924  dmiun  5926  dmuni  5927  dm0  5933  reldm0  5940  dmrnssfld  5986  dmcoss  5987  dmcosseq  5989  dmcosseqOLD  5990  dmres  6031  iss  6054  dmsnopg  6234  relssdmrnOLD  6290  funssres  6611  dmfco  7004  fiun  7965  f1iun  7966  frrlem8  8316  frrlem10  8318  wfrlem12OLD  8358  axdc3lem2  10488  fnpr2ob  17604  gsum2d2  20006  cnlnssadj  32108  prsdm  33874  eldm3  35740  dfdm5  35753  iss2  38325
  Copyright terms: Public domain W3C validator