Theorem eldm 5854

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

Syntax hints:   ↔ wb 206  ∃wex 1779   ∈ wcel 2109  Vcvv 3444   class class class wbr 5102  dom cdm 5631

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-dm 5641

This theorem is referenced by:  dmi  5875  dmep  5877  dmxp  5882  dmcoss  5927  dmcosseq  5929  dmcosseqOLD  5930  dminss  6114  dmsnn0  6168  dffun7  6527  dffun8  6528  fnres  6627  opabiota  6925  fndmdif  6996  dff3  7054  frxp  8082  suppvalbr  8120  reldmtpos  8190  dmtpos  8194  aceq3lem  10049  axdc2lem  10377  axdclem2  10449  fpwwe2lem11  10570  nqerf  10859  shftdm  15013  bcthlem4  25260  dchrisumlem3  27435  eulerpath  30220  fundmpss  35747  elfix  35884  fnsingle  35900  fnimage  35910  funpartlem  35923  dfrecs2  35931  dfrdg4  35932  knoppcnlem9  36482  prtlem16  38855  undmrnresiss  43586  isoval2  49017  termolmd  49652