Theorem eldm 5878

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

Syntax hints:   ↔ wb 208  ∃wex 1801   ∈ wcel 2144  Vcvv 3456   class class class wbr 5102  dom cdm 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-dm 5659

This theorem is referenced by:  dmi  5899  dmep  5901  dmxp  5907  dmcoss  5953  dmcossOLD  5954  dmcosseq  5956  dmcosseqOLD  5957  dmcosseqOLDOLD  5958  dminss  6140  dmsnn0  6196  dffun7  6550  dffun8  6551  fnres  6650  opabiota  6951  fndmdif  7025  dff3  7083  frxp  8108  suppvalbr  8146  reldmtpos  8216  dmtpos  8220  aceq3lem  10078  axdc2lem  10407  axdclem2  10479  fpwwe2lem11  10601  nqerf  10890  shftdm  15086  bcthlem4  25391  dchrisumlem3  27557  eulerpath  30445  fundmpss  36122  elfix  36256  fnsingle  36272  fnimage  36282  funpartlem  36297  dfrecs2  36305  dfrdg4  36306  knoppcnlem9  36944  prtlem16  39498  undmrnresiss  44185  isoval2  49661  termolmd  50296