Theorem eldm2 5850

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

Syntax hints:   ↔ wb 208  ∃wex 1787   ∈ wcel 2121  Vcvv 3433  ⟨cop 4564  dom cdm 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-dm 5631

This theorem is referenced by:  dmss  5851  opeldm  5856  dmin  5860  dmiun  5862  dmuni  5863  dm0  5869  reldm0  5877  dmrnssfld  5923  dmcoss  5924  dmcossOLD  5925  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  dmres  5971  iss  5994  dmsnopg  6168  funssres  6533  dmfco  6927  fiun  7889  f1iun  7890  frrlem8  8237  frrlem10  8239  axdc3lem2  10368  fnpr2ob  17517  gsum2d2  19944  cnlnssadj  32173  prsdm  34110  eldm3  36004  dfdm5  36016  iss2  38726