Theorem eldm 5881

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1811   ∈ wcel 2144  Vcvv 3450   class class class wbr 5102  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-dm 5660

This theorem is used by:  dmi  5902  dmep  5904  dmxp  5910  dmcoss  5956  dmcossOLD  5957  dmcosseq  5959  dmcosseqOLD  5960  dminss  6142  dmsnn0  6208  dffun7  6567  dffun8  6568  fnres  6666  opabiota  6967  fndmdif  7041  dff3  7100  frxp  8138  suppvalbr  8181  reldmtpos  8251  dmtpos  8255  aceq3lem  10199  axdc2lem  10526  axdclem2  10598  fpwwe2lem11  10726  nqerf  11015  shftdm  15224  bcthlem4  25648  dchrisumlem3  27818  eulerpath  30842  fundmpss  36532  elfix  36665  fnsingle  36681  fnimage  36691  funpartlem  36706  dfrecs2  36714  dfrdg4  36715  knoppcnlem9  37367  prtlem16  39927  undmrnresiss  44604  isoval2  50143  termolmd  50778