Theorem eldm 5353

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

Syntax hints:   ↔ wb 196  ∃wex 1744   ∈ wcel 2030  Vcvv 3231   class class class wbr 4685  dom cdm 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-dm 5153

This theorem is referenced by:  dmi  5372  dmcoss  5417  dmcosseq  5419  dminss  5582  dmsnn0  5635  dffun7  5953  dffun8  5954  fnres  6045  opabiota  6300  fndmdif  6361  dff3  6412  frxp  7332  suppvalbr  7344  reldmtpos  7405  dmtpos  7409  aceq3lem  8981  axdc2lem  9308  axdclem2  9380  fpwwe2lem12  9501  nqerf  9790  shftdm  13855  xpsfrnel2  16272  bcthlem4  23170  dchrisumlem3  25225  eulerpath  27219  fundmpss  31790  elfix  32135  fnsingle  32151  fnimage  32161  funpartlem  32174  dfrecs2  32182  dfrdg4  32183  knoppcnlem9  32616  prtlem16  34473  undmrnresiss  38227