Theorem eldm2 5855

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

Syntax hints:   ↔ wb 206  ∃wex 1779   ∈ wcel 2109  Vcvv 3444  ⟨cop 4591  dom cdm 5631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-dm 5641

This theorem is referenced by:  dmss  5856  opeldm  5861  dmin  5865  dmiun  5867  dmuni  5868  dm0  5874  reldm0  5881  dmrnssfld  5926  dmcoss  5927  dmcosseq  5929  dmcosseqOLD  5930  dmres  5972  iss  5995  dmsnopg  6174  relssdmrnOLD  6230  funssres  6544  dmfco  6939  fiun  7901  f1iun  7902  frrlem8  8249  frrlem10  8251  axdc3lem2  10380  fnpr2ob  17497  gsum2d2  19888  cnlnssadj  32059  prsdm  33897  eldm3  35741  dfdm5  35753  iss2  38319