MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsng Structured version   Visualization version   GIF version

Theorem fsng 7151
Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012.)
Assertion
Ref Expression
fsng ((𝐴𝐶𝐵𝐷) → (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {⟨𝐴, 𝐵⟩}))

Proof of Theorem fsng
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sneq 4643 . . . 4 (𝑎 = 𝐴 → {𝑎} = {𝐴})
21feq2d 6714 . . 3 (𝑎 = 𝐴 → (𝐹:{𝑎}⟶{𝑏} ↔ 𝐹:{𝐴}⟶{𝑏}))
3 opeq1 4879 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
43sneqd 4645 . . . 4 (𝑎 = 𝐴 → {⟨𝑎, 𝑏⟩} = {⟨𝐴, 𝑏⟩})
54eqeq2d 2737 . . 3 (𝑎 = 𝐴 → (𝐹 = {⟨𝑎, 𝑏⟩} ↔ 𝐹 = {⟨𝐴, 𝑏⟩}))
62, 5bibi12d 344 . 2 (𝑎 = 𝐴 → ((𝐹:{𝑎}⟶{𝑏} ↔ 𝐹 = {⟨𝑎, 𝑏⟩}) ↔ (𝐹:{𝐴}⟶{𝑏} ↔ 𝐹 = {⟨𝐴, 𝑏⟩})))
7 sneq 4643 . . . 4 (𝑏 = 𝐵 → {𝑏} = {𝐵})
87feq3d 6715 . . 3 (𝑏 = 𝐵 → (𝐹:{𝐴}⟶{𝑏} ↔ 𝐹:{𝐴}⟶{𝐵}))
9 opeq2 4880 . . . . 5 (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
109sneqd 4645 . . . 4 (𝑏 = 𝐵 → {⟨𝐴, 𝑏⟩} = {⟨𝐴, 𝐵⟩})
1110eqeq2d 2737 . . 3 (𝑏 = 𝐵 → (𝐹 = {⟨𝐴, 𝑏⟩} ↔ 𝐹 = {⟨𝐴, 𝐵⟩}))
128, 11bibi12d 344 . 2 (𝑏 = 𝐵 → ((𝐹:{𝐴}⟶{𝑏} ↔ 𝐹 = {⟨𝐴, 𝑏⟩}) ↔ (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {⟨𝐴, 𝐵⟩})))
13 vex 3466 . . 3 𝑎 ∈ V
14 vex 3466 . . 3 𝑏 ∈ V
1513, 14fsn 7149 . 2 (𝐹:{𝑎}⟶{𝑏} ↔ 𝐹 = {⟨𝑎, 𝑏⟩})
166, 12, 15vtocl2g 3555 1 ((𝐴𝐶𝐵𝐷) → (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {⟨𝐴, 𝐵⟩}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1534  wcel 2099  {csn 4633  cop 4639  wf 6550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5154  df-opab 5216  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561
This theorem is referenced by:  xpsng  7153  ftpg  7170  mapsnd  8915  axdc3lem4  10496  fseq1p1m1  13629  cats1un  14729  intopsn  18647  efmnd1bas  18883  grp1inv  19042  symg1bas  19388  esumsnf  33897  bnj149  34720  rngosn3  37625  sticksstones9  41852  sticksstones11  41854  k0004lem3  43816  ovnovollem1  46277  mapsnop  47723  snlindsntorlem  47853  lmod1zr  47876
  Copyright terms: Public domain W3C validator