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

Theorem eldm2 5912
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 5910 . 2 (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wex 1779  wcel 2108  Vcvv 3480  cop 4632  dom cdm 5685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-dm 5695
This theorem is referenced by:  dmss  5913  opeldm  5918  dmin  5922  dmiun  5924  dmuni  5925  dm0  5931  reldm0  5938  dmrnssfld  5984  dmcoss  5985  dmcosseq  5987  dmcosseqOLD  5988  dmres  6030  iss  6053  dmsnopg  6233  relssdmrnOLD  6289  funssres  6610  dmfco  7005  fiun  7967  f1iun  7968  frrlem8  8318  frrlem10  8320  wfrlem12OLD  8360  axdc3lem2  10491  fnpr2ob  17603  gsum2d2  19992  cnlnssadj  32099  prsdm  33913  eldm3  35761  dfdm5  35773  iss2  38345
  Copyright terms: Public domain W3C validator