Theorem eldm 5911

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

Syntax hints:   ↔ wb 206  ∃wex 1779   ∈ wcel 2108  Vcvv 3480   class class class wbr 5143  dom cdm 5685

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-dm 5695

This theorem is referenced by:  dmi  5932  dmep  5934  dmxp  5939  dmcoss  5985  dmcosseq  5987  dmcosseqOLD  5988  dminss  6173  dmsnn0  6227  dffun7  6593  dffun8  6594  fnres  6695  opabiota  6991  fndmdif  7062  dff3  7120  frxp  8151  suppvalbr  8189  reldmtpos  8259  dmtpos  8263  aceq3lem  10160  axdc2lem  10488  axdclem2  10560  fpwwe2lem11  10681  nqerf  10970  shftdm  15110  bcthlem4  25361  dchrisumlem3  27535  eulerpath  30260  fundmpss  35767  elfix  35904  fnsingle  35920  fnimage  35930  funpartlem  35943  dfrecs2  35951  dfrdg4  35952  knoppcnlem9  36502  prtlem16  38870  undmrnresiss  43617