Theorem dmsnopg 6216

Description: The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
dmsnopg	⊢ (𝐵 ∈ 𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴})

Proof of Theorem dmsnopg

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3461	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3461	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	opth1 5459	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
4	3	exlimiv 1963	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
5		opeq1 4840	. . . . 5 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩)
6		opeq2 4841	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝐵⟩)
7	6	eqeq1d 2767	. . . . . 6 ⊢ (𝑦 = 𝐵 → (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
8	7	spcegv 3558	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩ → ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
9	5, 8	syl5 35	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (𝑥 = 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
10	4, 9	impbid2 229	. . 3 ⊢ (𝐵 ∈ 𝑉 → (∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ 𝑥 = 𝐴))
11	1	eldm2 5893	. . . 4 ⊢ (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩})
12		opex 5447	. . . . . 6 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
13	12	elsn 4606	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
14	13	exbii 1881	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	11, 14	bitri 278	. . 3 ⊢ (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
16		velsn 4607	. . 3 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
17	10, 15, 16	3bitr4g 317	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ 𝑥 ∈ {𝐴}))
18	17	eqrdv 2763	1 ⊢ (𝐵 ∈ 𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴})

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∃wex 1812   ∈ wcel 2146  {csn 4591  ⟨cop 4597  dom cdm 5663

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-dm 5673

This theorem is used by:  dmsnopss  6217  dmpropg  6218  dmsnop  6219  rnsnopg  6224  fnsng  6592  funprg  6594  funtpg  6595  fntpg  6600  funsnfsupp  9355  s1dmALT  14663  setsval  17245  setsdm  17248  estrreslem2  18212  snstriedgval  29419  1loopgrvd0  29888  1hevtxdg0  29889  1hevtxdg1  29890  1egrvtxdg1  29893  p1evtxdeqlem  29896  wlkp1  30063  eupthp1  30614  trlsegvdeglem5  30622  cosnopne  33086  bnj96  35294  bnj535  35319  ovnovollem1  47403