Theorem eldm2 5879

Description: Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.)

Hypothesis

Ref	Expression
eldm.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
eldm2	⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵)

Distinct variable groups:   𝑦,𝐴   𝑦,𝐵

Proof of Theorem eldm2

Step	Hyp	Ref	Expression
1		eldm.1	. 2 ⊢ 𝐴 ∈ V
2		eldm2g 5877	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵)

Syntax hints:   ↔ wb 208  ∃wex 1801   ∈ wcel 2144  Vcvv 3456  ⟨cop 4590  dom cdm 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-dm 5659

This theorem is referenced by:  dmss  5880  opeldm  5885  dmin  5889  dmiun  5891  dmuni  5892  dm0  5898  reldm0  5906  dmrnssfld  5952  dmcoss  5953  dmcossOLD  5954  dmcosseq  5956  dmcosseqOLD  5957  dmcosseqOLDOLD  5958  dmres  6000  iss  6026  dmsnopg  6202  funssres  6567  dmfco  6965  fiun  7926  f1iun  7927  frrlem8  8276  frrlem10  8278  axdc3lem2  10410  fnpr2ob  17590  gsum2d2  20016  cnlnssadj  32285  prsdm  34213  eldm3  36116  dfdm5  36128  iss2  38848