Theorem opeldm 5889

Description: Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.)

Hypotheses

Ref	Expression
opeldm.1	⊢ 𝐴 ∈ V
opeldm.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
opeldm	⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶)

Proof of Theorem opeldm

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeldm.2	. . 3 ⊢ 𝐵 ∈ V
2		opeq2 4834	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
3	2	eleq1d 2846	. . 3 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝑦⟩ ∈ 𝐶 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝐶))
4	1, 3	spcev 3561	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐶)
5		opeldm.1	. . 3 ⊢ 𝐴 ∈ V
6	5	eldm2 5883	. 2 ⊢ (𝐴 ∈ dom 𝐶 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐶)
7	4, 6	sylibr 237	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3451  ⟨cop 4590  dom cdm 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5661

This theorem is used by:  breldm  5890  elreldm  5917  relssres  6011  iss  6027  dfrn7  6066  imadmrnOLD  6068  dfco2a  6247  relssdmrn  6271  funssres  6584  funun  6586  frxp2  8161  frxp3  8168  frrlem8  8311  frrlem10  8313  tz7.48-1  8453  iiner  8810  r0weon  10091  axdc3lem2  10529  uzrdgfni  14101  imasaddfnlem  17700  imasvscafn  17709  cicsym  17979  gsum2d  20186  noseqrdgfn  28692  cffldtocusgr  30028  dfcnv2  33269  gsumfs2d  33622  bnj1379  35460  iss2  39276  rfovcnvf1od  45003