Theorem eldm 5898

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

Syntax hints:   ↔ wb 205  ∃wex 1781   ∈ wcel 2106  Vcvv 3474   class class class wbr 5147  dom cdm 5675

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-dm 5685

This theorem is referenced by:  dmi  5919  dmep  5921  dmcoss  5968  dmcosseq  5970  dminss  6149  dmsnn0  6203  dffun7  6572  dffun8  6573  fnres  6674  opabiota  6971  fndmdif  7040  dff3  7098  frxp  8108  suppvalbr  8146  reldmtpos  8215  dmtpos  8219  aceq3lem  10111  axdc2lem  10439  axdclem2  10511  fpwwe2lem11  10632  nqerf  10921  shftdm  15014  bcthlem4  24835  dchrisumlem3  26983  eulerpath  29483  fundmpss  34726  elfix  34863  fnsingle  34879  fnimage  34889  funpartlem  34902  dfrecs2  34910  dfrdg4  34911  knoppcnlem9  35365  prtlem16  37727  undmrnresiss  42340