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  10051  axdc2lem  10379  axdclem2  10451  fpwwe2lem11  10572  nqerf  10861  shftdm  15014  bcthlem4  25261  dchrisumlem3  27436  eulerpath  30221  fundmpss  35748  elfix  35885  fnsingle  35901  fnimage  35911  funpartlem  35924  dfrecs2  35932  dfrdg4  35933  knoppcnlem9  36483  prtlem16  38856  undmrnresiss  43587  isoval2  49018  termolmd  49653