Theorem eldm 5755

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

Syntax hints:   ↔ wb 208  ∃wex 1780   ∈ wcel 2114  Vcvv 3486   class class class wbr 5052  dom cdm 5541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3488  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-sn 4554  df-pr 4556  df-op 4560  df-br 5053  df-dm 5551

This theorem is referenced by:  dmi  5777  dmep  5779  dmcoss  5828  dmcosseq  5830  dminss  5996  dmsnn0  6050  dffun7  6368  dffun8  6369  fnres  6460  opabiota  6732  fndmdif  6798  dff3  6852  frxp  7806  suppvalbr  7820  reldmtpos  7886  dmtpos  7890  aceq3lem  9532  axdc2lem  9856  axdclem2  9928  fpwwe2lem12  10049  nqerf  10338  shftdm  14415  bcthlem4  23913  dchrisumlem3  26053  eulerpath  28004  fundmpss  33016  elfix  33371  fnsingle  33387  fnimage  33397  funpartlem  33410  dfrecs2  33418  dfrdg4  33419  knoppcnlem9  33847  prtlem16  36037  undmrnresiss  40054