Theorem eldm 5809

Description: Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)

Hypothesis

Ref	Expression
eldm.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
eldm	⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)

Distinct variable groups:   𝑦,𝐴   𝑦,𝐵

Proof of Theorem eldm

Step	Hyp	Ref	Expression
1		eldm.1	. 2 ⊢ 𝐴 ∈ V
2		eldmg 5807	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)

Syntax hints:   ↔ wb 205  ∃wex 1782   ∈ wcel 2106  Vcvv 3432   class class class wbr 5074  dom cdm 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-dm 5599

This theorem is referenced by:  dmi  5830  dmep  5832  dmcoss  5880  dmcosseq  5882  dminss  6056  dmsnn0  6110  dffun7  6461  dffun8  6462  fnres  6559  opabiota  6851  fndmdif  6919  dff3  6976  frxp  7967  suppvalbr  7981  reldmtpos  8050  dmtpos  8054  aceq3lem  9876  axdc2lem  10204  axdclem2  10276  fpwwe2lem11  10397  nqerf  10686  shftdm  14782  bcthlem4  24491  dchrisumlem3  26639  eulerpath  28605  fundmpss  33740  elfix  34205  fnsingle  34221  fnimage  34231  funpartlem  34244  dfrecs2  34252  dfrdg4  34253  knoppcnlem9  34681  prtlem16  36883  undmrnresiss  41212