Theorem eldm 5888

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1812   ∈ wcel 2147  Vcvv 3454   class class class wbr 5106  dom cdm 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-dm 5665

This theorem is used by:  dmi  5909  dmep  5911  dmxp  5917  dmcoss  5963  dmcossOLD  5964  dmcosseq  5966  dmcosseqOLD  5967  dminss  6154  dmsnn0  6220  idresdmsscocnv1  6274  dffun7  6584  dffun8  6585  fnres  6685  opabiota  6987  fndmdif  7061  dff3  7121  frxp  8162  suppvalbr  8205  suppvalbrOLD  8206  reldmtpos  8276  dmtpos  8280  aceq3lem  10223  axdc2lem  10550  axdclem2  10622  fpwwe2lem11  10750  nqerf  11039  shftdm  15250  bcthlem4  25675  dchrisumlem3  27845  eulerpath  30869  fundmpss  36709  elfix  36842  fnsingle  36858  fnimage  36868  funpartlem  36883  dfrecs2  36891  dfrdg4  36892  knoppcnlem9  37544  prtlem16  40117  undmrnresiss  44794  isoval2  50352  termolmd  51056