Theorem eldm 5848

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

Syntax hints:   ↔ wb 208  ∃wex 1787   ∈ wcel 2121  Vcvv 3433   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 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  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  5869  dmep  5871  dmxp  5877  dmcoss  5923  dmcossOLD  5924  dmcosseq  5926  dmcosseqOLD  5927  dmcosseqOLDOLD  5928  dminss  6107  dmsnn0  6161  dffun7  6515  dffun8  6516  fnres  6615  opabiota  6912  fndmdif  6986  dff3  7044  frxp  8068  suppvalbr  8106  reldmtpos  8176  dmtpos  8180  aceq3lem  10037  axdc2lem  10366  axdclem2  10438  fpwwe2lem11  10560  nqerf  10849  shftdm  15028  bcthlem4  25315  dchrisumlem3  27475  eulerpath  30331  fundmpss  36008  elfix  36142  fnsingle  36158  fnimage  36168  funpartlem  36183  dfrecs2  36191  dfrdg4  36192  knoppcnlem9  36820  prtlem16  39374  undmrnresiss  44061  isoval2  49537  termolmd  50172