Theorem dmsnopg 6070

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 3497	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3497	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	opth1 5367	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
4	3	exlimiv 1931	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑥 = 𝐴)
5		opeq1 4803	. . . . 5 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩)
6		opeq2 4804	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝐵⟩)
7	6	eqeq1d 2823	. . . . . 6 ⊢ (𝑦 = 𝐵 → (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ ⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
8	7	spcegv 3597	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (⟨𝑥, 𝐵⟩ = ⟨𝐴, 𝐵⟩ → ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
9	5, 8	syl5 34	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (𝑥 = 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩))
10	4, 9	impbid2 228	. . 3 ⊢ (𝐵 ∈ 𝑉 → (∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ 𝑥 = 𝐴))
11	1	eldm2 5770	. . . 4 ⊢ (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩})
12		opex 5356	. . . . . 6 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
13	12	elsn 4582	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
14	13	exbii 1848	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	11, 14	bitri 277	. . 3 ⊢ (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ ∃𝑦⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
16		velsn 4583	. . 3 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
17	10, 15, 16	3bitr4g 316	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ dom {⟨𝐴, 𝐵⟩} ↔ 𝑥 ∈ {𝐴}))
18	17	eqrdv 2819	1 ⊢ (𝐵 ∈ 𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴})

Syntax hints:   → wi 4   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {csn 4567  ⟨cop 4573  dom cdm 5555

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-dm 5565

This theorem is referenced by:  dmsnopss  6071  dmpropg  6072  dmsnop  6073  rnsnopg  6078  fnsng  6406  funprg  6408  funtpg  6409  fntpg  6414  funsnfsupp  8857  s1dmALT  13963  setsval  16513  setsdm  16517  estrreslem2  17388  snstriedgval  26823  1loopgrvd0  27286  1hevtxdg0  27287  1hevtxdg1  27288  1egrvtxdg1  27291  p1evtxdeqlem  27294  wlkp1  27463  eupthp1  27995  trlsegvdeglem5  28003  cosnopne  30430  bnj96  32137  bnj535  32162  ovnovollem1  42958