Theorem eldm 5844

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 5842	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)

Syntax hints:   ↔ wb 206  ∃wex 1781   ∈ wcel 2114  Vcvv 3427   class class class wbr 5074  dom cdm 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-dm 5630

This theorem is referenced by:  dmi  5865  dmep  5867  dmxp  5873  dmcoss  5919  dmcossOLD  5920  dmcosseq  5922  dmcosseqOLD  5923  dmcosseqOLDOLD  5924  dminss  6106  dmsnn0  6160  dffun7  6514  dffun8  6515  fnres  6614  opabiota  6911  fndmdif  6983  dff3  7041  frxp  8065  suppvalbr  8103  reldmtpos  8173  dmtpos  8177  aceq3lem  10031  axdc2lem  10359  axdclem2  10431  fpwwe2lem11  10553  nqerf  10842  shftdm  15022  bcthlem4  25282  dchrisumlem3  27442  eulerpath  30299  fundmpss  35937  elfix  36071  fnsingle  36087  fnimage  36097  funpartlem  36112  dfrecs2  36120  dfrdg4  36121  knoppcnlem9  36749  prtlem16  39303  undmrnresiss  44019  isoval2  49498  termolmd  50133