Theorem eldm2 5890

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1808   ∈ wcel 2142  Vcvv 3454  ⟨cop 4594  dom cdm 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-dm 5670

This theorem is used by:  dmss  5891  opeldm  5896  dmin  5900  dmiun  5902  dmuni  5903  dm0  5909  reldm0  5917  dmrnssfld  5963  dmcoss  5964  dmcossOLD  5965  dmcosseq  5967  dmcosseqOLD  5968  dmres  6010  iss  6036  dmsnopg  6213  funssres  6580  dmfco  6977  fiun  7938  f1iun  7939  frrlem8  8288  frrlem10  8290  axdc3lem2  10441  fnpr2ob  17618  gsum2d2  20050  cnlnssadj  32443  prsdm  34313  eldm3  36261  dfdm5  36273  iss2  39021