Theorem f1osng 6868

Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013.)

Assertion

Ref	Expression
f1osng	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})

Proof of Theorem f1osng

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sneq 4590	. . . 4 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
2	1	f1oeq2d 6821	. . 3 ⊢ (𝑎 = 𝐴 → ({⟨𝑎, 𝑏⟩}:{𝑎}–1-1-onto→{𝑏} ↔ {⟨𝑎, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏}))
3		opeq1 4839	. . . . 5 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
4	3	sneqd 4592	. . . 4 ⊢ (𝑎 = 𝐴 → {⟨𝑎, 𝑏⟩} = {⟨𝐴, 𝑏⟩})
5	4	f1oeq1d 6820	. . 3 ⊢ (𝑎 = 𝐴 → ({⟨𝑎, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏} ↔ {⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏}))
6	2, 5	bitrd 282	. 2 ⊢ (𝑎 = 𝐴 → ({⟨𝑎, 𝑏⟩}:{𝑎}–1-1-onto→{𝑏} ↔ {⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏}))
7		sneq 4590	. . . 4 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
8	7	f1oeq3d 6822	. . 3 ⊢ (𝑏 = 𝐵 → ({⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏} ↔ {⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝐵}))
9		opeq2 4840	. . . . 5 ⊢ (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
10	9	sneqd 4592	. . . 4 ⊢ (𝑏 = 𝐵 → {⟨𝐴, 𝑏⟩} = {⟨𝐴, 𝐵⟩})
11	10	f1oeq1d 6820	. . 3 ⊢ (𝑏 = 𝐵 → ({⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝐵} ↔ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}))
12	8, 11	bitrd 282	. 2 ⊢ (𝑏 = 𝐵 → ({⟨𝐴, 𝑏⟩}:{𝐴}–1-1-onto→{𝑏} ↔ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}))
13		vex 3454	. . 3 ⊢ 𝑎 ∈ V
14		vex 3454	. . 3 ⊢ 𝑏 ∈ V
15	13, 14	f1osn 6867	. 2 ⊢ {⟨𝑎, 𝑏⟩}:{𝑎}–1-1-onto→{𝑏}
16	6, 12, 15	vtocl2g 3533	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {csn 4584  ⟨cop 4834  –1-1-onto→wf1o 6538

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  ax-sep 5248  ax-pr 5390

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-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546

This theorem is used by:  f1sng  6869  f1oprswap  6871  f1oprg  6872  f1o2sn  7146  fsnunf  7191  fsnex  7292  suppsnop  8199  mapsnd  8918  ralxpmap  8928  en2sn  9073  enfixsn  9109  fseqenlem1  10107  canthp1lem2  10742  s1f1  14761  sumsnf  15915  prodsn  16135  prodsnf  16137  vdwlem8  17172  gsumws1  19040  symg1bas  19611  dprdsn  20258  eupthp1  30823  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  mapfzcons  43821  sumsnd  46137  1hegrlfgr  49324