Theorem dmsnopg 6155

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 3440	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3440	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	opth1 5410	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
4	3	exlimiv 1931	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
5		opeq1 4820	. . . . 5 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩)
6		opeq2 4821	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝐵⟩)
7	6	eqeq1d 2733	. . . . . 6 ⊢ (𝑦 = 𝐵 → (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
8	7	spcegv 3547	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩ → ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
9	5, 8	syl5 34	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (𝑥 = 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
10	4, 9	impbid2 226	. . 3 ⊢ (𝐵 ∈ 𝑉 → (∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ 𝑥 = 𝐴))
11	1	eldm2 5836	. . . 4 ⊢ (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩})
12		opex 5399	. . . . . 6 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
13	12	elsn 4586	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
14	13	exbii 1849	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	11, 14	bitri 275	. . 3 ⊢ (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
16		velsn 4587	. . 3 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
17	10, 15, 16	3bitr4g 314	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ 𝑥 ∈ {𝐴}))
18	17	eqrdv 2729	1 ⊢ (𝐵 ∈ 𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴})

Syntax hints:   → wi 4   = wceq 1541  ∃wex 1780   ∈ wcel 2111  {csn 4571  ⟨cop 4577  dom cdm 5611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-dm 5621

This theorem is referenced by:  dmsnopss  6156  dmpropg  6157  dmsnop  6158  rnsnopg  6163  fnsng  6528  funprg  6530  funtpg  6531  fntpg  6536  funsnfsupp  9271  s1dmALT  14512  setsval  17073  setsdm  17076  estrreslem2  18039  snstriedgval  29011  1loopgrvd0  29478  1hevtxdg0  29479  1hevtxdg1  29480  1egrvtxdg1  29483  p1evtxdeqlem  29486  wlkp1  29653  eupthp1  30188  trlsegvdeglem5  30196  cosnopne  32667  bnj96  34869  bnj535  34894  ovnovollem1  46694