Theorem eldm 5879

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1812   ∈ wcel 2145  Vcvv 3450   class class class wbr 5103  dom cdm 5648

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5658

This theorem is used by:  dmi  5900  dmep  5902  dmxp  5908  dmcoss  5954  dmcossOLD  5955  dmcosseq  5957  dmcosseqOLD  5958  dminss  6139  dmsnn0  6198  dffun7  6556  dffun8  6557  fnres  6655  opabiota  6956  fndmdif  7030  dff3  7089  frxp  8122  suppvalbr  8160  reldmtpos  8230  dmtpos  8234  aceq3lem  10156  axdc2lem  10483  axdclem2  10555  fpwwe2lem11  10683  nqerf  10972  shftdm  15177  bcthlem4  25595  dchrisumlem3  27767  eulerpath  30761  fundmpss  36447  elfix  36581  fnsingle  36597  fnimage  36607  funpartlem  36622  dfrecs2  36630  dfrdg4  36631  knoppcnlem9  37283  prtlem16  39840  undmrnresiss  44542  isoval2  50059  termolmd  50694