Theorem eldm 5889

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1808   ∈ wcel 2142  Vcvv 3454   class class class wbr 5108  dom cdm 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-dm 5670

This theorem is used by:  dmi  5910  dmep  5912  dmxp  5918  dmcoss  5964  dmcossOLD  5965  dmcosseq  5967  dmcosseqOLD  5968  dminss  6149  dmsnn0  6207  dffun7  6563  dffun8  6564  fnres  6662  opabiota  6963  fndmdif  7037  dff3  7095  frxp  8120  suppvalbr  8158  reldmtpos  8228  dmtpos  8232  aceq3lem  10111  axdc2lem  10438  axdclem2  10510  fpwwe2lem11  10632  nqerf  10921  shftdm  15115  bcthlem4  25497  dchrisumlem3  27666  eulerpath  30603  fundmpss  36267  elfix  36401  fnsingle  36417  fnimage  36427  funpartlem  36442  dfrecs2  36450  dfrdg4  36451  knoppcnlem9  37118  prtlem16  39671  undmrnresiss  44358  isoval2  49841  termolmd  50476