Theorem f1osn 6808

Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by NM, 18-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Hypotheses

Ref	Expression
f1osn.1	⊢ 𝐴 ∈ V
f1osn.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
f1osn	⊢ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}

Proof of Theorem f1osn

Step	Hyp	Ref	Expression
1		f1osn.1	. . 3 ⊢ 𝐴 ∈ V
2		f1osn.2	. . 3 ⊢ 𝐵 ∈ V
3	1, 2	fnsn 6543	. 2 ⊢ {⟨𝐴, 𝐵⟩} Fn {𝐴}
4	2, 1	fnsn 6543	. . 3 ⊢ {⟨𝐵, 𝐴⟩} Fn {𝐵}
5	1, 2	cnvsn 6177	. . . 4 ⊢ ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩}
6	5	fneq1i 6582	. . 3 ⊢ (◡{⟨𝐴, 𝐵⟩} Fn {𝐵} ↔ {⟨𝐵, 𝐴⟩} Fn {𝐵})
7	4, 6	mpbir 232	. 2 ⊢ ◡{⟨𝐴, 𝐵⟩} Fn {𝐵}
8		dff1o4 6775	. 2 ⊢ ({⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵} ↔ ({⟨𝐴, 𝐵⟩} Fn {𝐴} ∧ ◡{⟨𝐴, 𝐵⟩} Fn {𝐵}))
9	3, 7, 8	mpbir2an 717	1 ⊢ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}

Syntax hints:   ∈ wcel 2119  Vcvv 3431  {csn 4555  ⟨cop 4561  ^◡ccnv 5617   Fn wfn 6480  –1-1-onto→wf1o 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492

This theorem is referenced by:  f1osng  6809  fsn  7077  ensn1  8958  pssnn  9093  isinf  9165  ac6sfi  9184  marypha1lem  9336  hashf1lem1  14408  0ram  16982  mdet0f1o  22576  imasdsf1olem  24356  istrkg2ld  28546  axlowdimlem10  29038  selvply1rhmlemb  33703  subfacp1lem5  35412  poimirlem3  37990  grposnOLD  38249