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

Theorem f1oeq3 6838
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 6801 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶1-1𝐴𝐹:𝐶1-1𝐵))
2 foeq3 6818 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
31, 2anbi12d 632 . 2 (𝐴 = 𝐵 → ((𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴) ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵)))
4 df-f1o 6568 . 2 (𝐹:𝐶1-1-onto𝐴 ↔ (𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴))
5 df-f1o 6568 . 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 206  wa 395   = wceq 1540  1-1wf1 6558  ontowfo 6559  1-1-ontowf1o 6560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568
This theorem is referenced by:  f1oeq23  6839  f1oeq123d  6842  f1oeq3d  6845  f1ores  6862  resin  6870  isoeq5  7341  breng  8994  xpcomf1o  9101  isinf  9296  isinfOLD  9297  cnfcom2  9742  fin1a2lem6  10445  pwfseqlem5  10703  pwfseq  10704  hashgf1o  14012  axdc4uzlem  14024  sumeq1  15725  prodeq1f  15942  prodeq1  15943  prodeq1i  15952  unbenlem  16946  4sqlem11  16993  gsumvalx  18689  cayley  19432  cayleyth  19433  ovolicc2lem4  25555  logf1o2  26692  uspgrf1oedg  29190  uspgredgiedg  29192  wlkiswwlks2lem4  29892  clwwlknonclwlknonf1o  30381  dlwwlknondlwlknonf1o  30384  adjbd1o  32104  rinvf1o  32640  cshf1o  32947  eulerpartgbij  34374  eulerpartlemgh  34380  derangval  35172  subfacp1lem2a  35185  subfacp1lem3  35187  subfacp1lem5  35189  mrsubff1o  35520  msubff1o  35562  cbvprodvw2  36248  bj-finsumval0  37286  f1omptsnlem  37337  f1omptsn  37338  poimirlem9  37636  poimirlem15  37642  ismtyval  37807  ismrer1  37845  lautset  40084  pautsetN  40100  hvmap1o2  41767  pwfi2f1o  43108  imasgim  43112  alephiso2  43571  f1ocof1ob2  47094  isuspgrim0lem  47871  gricushgr  47886  grtriprop  47908  grtrif1o  47909  isgrtri  47910  uspgrsprfo  48064
  Copyright terms: Public domain W3C validator