Theorem eldm 5843

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

Syntax hints:   ↔ wb 206  ∃wex 1779   ∈ wcel 2109  Vcvv 3436   class class class wbr 5092  dom cdm 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-dm 5629

This theorem is referenced by:  dmi  5864  dmep  5866  dmxp  5871  dmcoss  5916  dmcossOLD  5917  dmcosseq  5919  dmcosseqOLD  5920  dmcosseqOLDOLD  5921  dminss  6102  dmsnn0  6156  dffun7  6509  dffun8  6510  fnres  6609  opabiota  6905  fndmdif  6976  dff3  7034  frxp  8059  suppvalbr  8097  reldmtpos  8167  dmtpos  8171  aceq3lem  10014  axdc2lem  10342  axdclem2  10414  fpwwe2lem11  10535  nqerf  10824  shftdm  14978  bcthlem4  25225  dchrisumlem3  27400  eulerpath  30189  fundmpss  35760  elfix  35897  fnsingle  35913  fnimage  35923  funpartlem  35936  dfrecs2  35944  dfrdg4  35945  knoppcnlem9  36495  prtlem16  38868  undmrnresiss  43597  isoval2  49040  termolmd  49675