Theorem eldm 5566

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

Syntax hints:   ↔ wb 198  ∃wex 1823   ∈ wcel 2107  Vcvv 3398   class class class wbr 4886  dom cdm 5355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-dm 5365

This theorem is referenced by:  dmi  5585  dmcoss  5631  dmcosseq  5633  dminss  5801  dmsnn0  5854  dffun7  6162  dffun8  6163  fnres  6253  opabiota  6521  fndmdif  6584  dff3  6636  frxp  7568  suppvalbr  7580  reldmtpos  7642  dmtpos  7646  aceq3lem  9276  axdc2lem  9605  axdclem2  9677  fpwwe2lem12  9798  nqerf  10087  shftdm  14218  xpsfrnel2  16611  bcthlem4  23533  dchrisumlem3  25632  eulerpath  27645  fundmpss  32257  elfix  32599  fnsingle  32615  fnimage  32625  funpartlem  32638  dfrecs2  32646  dfrdg4  32647  knoppcnlem9  33074  prtlem16  35023  undmrnresiss  38867