Theorem eldm2 5889

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

Syntax hints:   ↔ wb 209  ∃wex 1806   ∈ wcel 2149  Vcvv 3463  ⟨cop 4597  dom cdm 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-dm 5669

This theorem is referenced by:  dmss  5890  opeldm  5895  dmin  5899  dmiun  5901  dmuni  5902  dm0  5908  reldm0  5916  dmrnssfld  5962  dmcoss  5963  dmcossOLD  5964  dmcosseq  5966  dmcosseqOLD  5967  dmres  6009  iss  6035  dmsnopg  6211  funssres  6577  dmfco  6975  fiun  7936  f1iun  7937  frrlem8  8286  frrlem10  8288  axdc3lem2  10431  fnpr2ob  17608  gsum2d2  20040  cnlnssadj  32369  prsdm  34245  eldm3  36148  dfdm5  36160  iss2  38878