Theorem eldm 5733

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

Syntax hints:   ↔ wb 209  ∃wex 1781   ∈ wcel 2111  Vcvv 3441   class class class wbr 5030  dom cdm 5519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-dm 5529

This theorem is referenced by:  dmi  5755  dmep  5757  dmcoss  5807  dmcosseq  5809  dminss  5977  dmsnn0  6031  dffun7  6351  dffun8  6352  fnres  6446  opabiota  6721  fndmdif  6789  dff3  6843  frxp  7803  suppvalbr  7817  reldmtpos  7883  dmtpos  7887  aceq3lem  9531  axdc2lem  9859  axdclem2  9931  fpwwe2lem12  10052  nqerf  10341  shftdm  14422  bcthlem4  23931  dchrisumlem3  26075  eulerpath  28026  fundmpss  33122  elfix  33477  fnsingle  33493  fnimage  33503  funpartlem  33516  dfrecs2  33524  dfrdg4  33525  knoppcnlem9  33953  prtlem16  36165  undmrnresiss  40304