Theorem eldm 5890

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

Syntax hints:   ↔ wb 209  ∃wex 1807   ∈ wcel 2141  Vcvv 3453   class class class wbr 5108  dom cdm 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-dm 5671

This theorem is referenced by:  dmi  5911  dmep  5913  dmxp  5919  dmcoss  5965  dmcossOLD  5966  dmcosseq  5968  dmcosseqOLD  5969  dminss  6150  dmsnn0  6208  dffun7  6563  dffun8  6564  fnres  6662  opabiota  6963  fndmdif  7037  dff3  7095  frxp  8121  suppvalbr  8159  reldmtpos  8229  dmtpos  8233  aceq3lem  10103  axdc2lem  10431  axdclem2  10503  fpwwe2lem11  10625  nqerf  10914  shftdm  15107  bcthlem4  25465  dchrisumlem3  27631  eulerpath  30558  fundmpss  36213  elfix  36347  fnsingle  36363  fnimage  36373  funpartlem  36388  dfrecs2  36396  dfrdg4  36397  knoppcnlem9  37034  prtlem16  39589  undmrnresiss  44278  isoval2  49758  termolmd  50393