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

Theorem eldm2 5769
 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 5767 . 2 (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207  ∃wex 1773   ∈ wcel 2107  Vcvv 3500  ⟨cop 4570  dom cdm 5554 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-dm 5564 This theorem is referenced by:  dmss  5770  opeldm  5775  dmin  5779  dmiun  5781  dmuni  5782  dm0  5789  reldm0  5797  dmrnssfld  5840  dmcoss  5841  dmcosseq  5843  dmres  5874  iss  5902  dmsnopg  6069  relssdmrn  6120  funssres  6397  dmfco  6756  fiunw  7637  f1iunw  7638  fiun  7640  f1iun  7641  wfrlem12  7962  axdc3lem2  9867  fnpr2ob  16826  gsum2d2  19030  cnlnssadj  29790  prsdm  31062  eldm3  32900  dfdm5  32919  frrlem8  33033  frrlem10  33035  iss2  35488
 Copyright terms: Public domain W3C validator