Theorem eldm 5867

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

Syntax hints:   ↔ wb 206  ∃wex 1779   ∈ wcel 2109  Vcvv 3450   class class class wbr 5110  dom cdm 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-dm 5651

This theorem is referenced by:  dmi  5888  dmep  5890  dmxp  5895  dmcoss  5941  dmcosseq  5943  dmcosseqOLD  5944  dminss  6129  dmsnn0  6183  dffun7  6546  dffun8  6547  fnres  6648  opabiota  6946  fndmdif  7017  dff3  7075  frxp  8108  suppvalbr  8146  reldmtpos  8216  dmtpos  8220  aceq3lem  10080  axdc2lem  10408  axdclem2  10480  fpwwe2lem11  10601  nqerf  10890  shftdm  15044  bcthlem4  25234  dchrisumlem3  27409  eulerpath  30177  fundmpss  35761  elfix  35898  fnsingle  35914  fnimage  35924  funpartlem  35937  dfrecs2  35945  dfrdg4  35946  knoppcnlem9  36496  prtlem16  38869  undmrnresiss  43600  isoval2  49028  termolmd  49663