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

Theorem eldm2 5523
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 5521 . 2 (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ dom 𝐵 ↔ ∃𝑦𝐴, 𝑦⟩ ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wex 1859  wcel 2156  Vcvv 3391  cop 4376  dom cdm 5311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845  df-dm 5321
This theorem is referenced by:  dmss  5524  opeldm  5529  dmin  5533  dmiun  5534  dmuni  5535  dm0  5540  reldm0  5544  dmrnssfld  5585  dmcoss  5586  dmcosseq  5588  dmres  5622  iss  5652  dmsnopg  5818  relssdmrn  5870  funssres  6140  dmfco  6489  fun11iun  7352  wfrlem12  7658  axdc3lem2  9554  gsum2d2  18570  cnlnssadj  29263  prsdm  30281  eldm3  31968  dfdm5  31991  frrlem11  32108  iss2  34420
  Copyright terms: Public domain W3C validator