Theorem eldm 5848

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

Syntax hints:   ↔ wb 206  ∃wex 1781   ∈ wcel 2114  Vcvv 3439   class class class wbr 5097  dom cdm 5623

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-dm 5633

This theorem is referenced by:  dmi  5869  dmep  5871  dmxp  5877  dmcoss  5923  dmcossOLD  5924  dmcosseq  5926  dmcosseqOLD  5927  dmcosseqOLDOLD  5928  dminss  6110  dmsnn0  6164  dffun7  6518  dffun8  6519  fnres  6618  opabiota  6915  fndmdif  6987  dff3  7045  frxp  8068  suppvalbr  8106  reldmtpos  8176  dmtpos  8180  aceq3lem  10032  axdc2lem  10360  axdclem2  10432  fpwwe2lem11  10554  nqerf  10843  shftdm  14996  bcthlem4  25285  dchrisumlem3  27460  eulerpath  30297  fundmpss  35940  elfix  36074  fnsingle  36090  fnimage  36100  funpartlem  36115  dfrecs2  36123  dfrdg4  36124  knoppcnlem9  36674  prtlem16  39164  undmrnresiss  43882  isoval2  49317  termolmd  49952