Theorem eldm2 5882

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1811   ∈ wcel 2144  Vcvv 3450  ⟨cop 4589  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-dm 5660

This theorem is used by:  dmss  5883  opeldm  5888  dmin  5892  dmiun  5894  dmuni  5895  dm0  5901  reldm0  5909  dmrnssfld  5955  dmcoss  5956  dmcossOLD  5957  dmcosseq  5959  dmcosseqOLD  5960  dmres  6002  iss  6026  dmsnopg  6214  funssres  6584  dmfco  6981  fiun  7955  f1iun  7956  frrlem8  8311  frrlem10  8313  axdc3lem2  10529  fnpr2ob  17730  gsum2d2  20188  cnlnssadj  32682  prsdm  34546  eldm3  36526  dfdm5  36537  iss2  39277