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

Theorem f1oeq3 6775
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq3 (𝐴 = 𝐵 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))

Proof of Theorem f1oeq3
StepHypRef Expression
1 f1eq3 6736 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶1-1𝐴𝐹:𝐶1-1𝐵))
2 foeq3 6755 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
31, 2anbi12d 632 . 2 (𝐴 = 𝐵 → ((𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴) ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵)))
4 df-f1o 6504 . 2 (𝐹:𝐶1-1-onto𝐴 ↔ (𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴))
5 df-f1o 6504 . 2 (𝐹:𝐶1-1-onto𝐵 ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵))
63, 4, 53bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  1-1wf1 6494  ontowfo 6495  1-1-ontowf1o 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504
This theorem is referenced by:  f1oeq23  6776  f1oeq123d  6779  f1oeq3d  6782  f1ores  6799  resin  6807  isoeq5  7267  breng  8893  brenOLD  8895  xpcomf1o  9006  isinf  9205  isinfOLD  9206  cnfcom2  9639  fin1a2lem6  10342  pwfseqlem5  10600  pwfseq  10601  hashgf1o  13877  axdc4uzlem  13889  sumeq1  15574  prodeq1f  15792  unbenlem  16781  4sqlem11  16828  gsumvalx  18532  cayley  19197  cayleyth  19198  ovolicc2lem4  24887  logf1o2  26008  uspgrf1oedg  28127  wlkiswwlks2lem4  28820  clwwlknonclwlknonf1o  29309  dlwwlknondlwlknonf1o  29312  adjbd1o  31030  rinvf1o  31547  cshf1o  31819  eulerpartgbij  32975  eulerpartlemgh  32981  derangval  33764  subfacp1lem2a  33777  subfacp1lem3  33779  subfacp1lem5  33781  mrsubff1o  34112  msubff1o  34154  bj-finsumval0  35759  f1omptsnlem  35810  f1omptsn  35811  poimirlem9  36090  poimirlem15  36096  ismtyval  36262  ismrer1  36300  lautset  38548  pautsetN  38564  hvmap1o2  40231  pwfi2f1o  41426  imasgim  41430  alephiso2  41837  f1ocof1ob2  45321  isomushgr  46025  uspgrsprfo  46057
  Copyright terms: Public domain W3C validator