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

Theorem f1osn 6653
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
StepHypRef Expression
1 f1osn.1 . . 3 𝐴 ∈ V
2 f1osn.2 . . 3 𝐵 ∈ V
31, 2fnsn 6411 . 2 {⟨𝐴, 𝐵⟩} Fn {𝐴}
42, 1fnsn 6411 . . 3 {⟨𝐵, 𝐴⟩} Fn {𝐵}
51, 2cnvsn 6082 . . . 4 {⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩}
65fneq1i 6449 . . 3 ({⟨𝐴, 𝐵⟩} Fn {𝐵} ↔ {⟨𝐵, 𝐴⟩} Fn {𝐵})
74, 6mpbir 232 . 2 {⟨𝐴, 𝐵⟩} Fn {𝐵}
8 dff1o4 6622 . 2 ({⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵} ↔ ({⟨𝐴, 𝐵⟩} Fn {𝐴} ∧ {⟨𝐴, 𝐵⟩} Fn {𝐵}))
93, 7, 8mpbir2an 707 1 {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3500  {csn 4564  cop 4570  ccnv 5553   Fn wfn 6349  1-1-ontowf1o 6353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361
This theorem is referenced by:  f1osng  6654  fsn  6895  ensn1  8567  phplem2  8691  isinf  8725  pssnn  8730  ac6sfi  8756  marypha1lem  8891  hashf1lem1  13808  0ram  16351  mdet0f1o  21137  imasdsf1olem  22917  istrkg2ld  26179  axlowdimlem10  26670  subfacp1lem5  32334  poimirlem3  34781  grposnOLD  35047
  Copyright terms: Public domain W3C validator