Theorem eldm 5901

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

Syntax hints:   ↔ wb 205  ∃wex 1782   ∈ wcel 2107  Vcvv 3475   class class class wbr 5149  dom cdm 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-dm 5687

This theorem is referenced by:  dmi  5922  dmep  5924  dmcoss  5971  dmcosseq  5973  dminss  6153  dmsnn0  6207  dffun7  6576  dffun8  6577  fnres  6678  opabiota  6975  fndmdif  7044  dff3  7102  frxp  8112  suppvalbr  8150  reldmtpos  8219  dmtpos  8223  aceq3lem  10115  axdc2lem  10443  axdclem2  10515  fpwwe2lem11  10636  nqerf  10925  shftdm  15018  bcthlem4  24844  dchrisumlem3  26994  eulerpath  29494  fundmpss  34738  elfix  34875  fnsingle  34891  fnimage  34901  funpartlem  34914  dfrecs2  34922  dfrdg4  34923  knoppcnlem9  35377  prtlem16  37739  undmrnresiss  42355