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

Theorem f1oeq3 6585
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 6550 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶1-1𝐴𝐹:𝐶1-1𝐵))
2 foeq3 6567 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
31, 2anbi12d 633 . 2 (𝐴 = 𝐵 → ((𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴) ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵)))
4 df-f1o 6335 . 2 (𝐹:𝐶1-1-onto𝐴 ↔ (𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴))
5 df-f1o 6335 . 2 (𝐹:𝐶1-1-onto𝐵 ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵))
63, 4, 53bitr4g 317 1 (𝐴 = 𝐵 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  1-1wf1 6325  ontowfo 6326  1-1-ontowf1o 6327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335
This theorem is referenced by:  f1oeq23  6586  f1oeq123d  6589  f1oeq3d  6591  f1ores  6608  resin  6615  isoeq5  7057  bren  8505  xpcomf1o  8593  isinf  8719  cnfcom2  9153  fin1a2lem6  9820  pwfseqlem5  10078  pwfseq  10079  hashgf1o  13338  axdc4uzlem  13350  sumeq1  15041  prodeq1f  15258  unbenlem  16238  4sqlem11  16285  gsumvalx  17882  cayley  18538  cayleyth  18539  ovolicc2lem4  24128  logf1o2  25245  uspgrf1oedg  26970  wlkiswwlks2lem4  27662  clwwlknonclwlknonf1o  28151  dlwwlknondlwlknonf1o  28154  adjbd1o  29872  rinvf1o  30393  cshf1o  30666  eulerpartgbij  31744  eulerpartlemgh  31750  derangval  32528  subfacp1lem2a  32541  subfacp1lem3  32543  subfacp1lem5  32545  mrsubff1o  32876  msubff1o  32918  bj-finsumval0  34701  f1omptsnlem  34754  f1omptsn  34755  poimirlem4  35060  poimirlem9  35065  poimirlem15  35071  ismtyval  35237  ismrer1  35275  lautset  37377  pautsetN  37393  hvmap1o2  39060  pwfi2f1o  40033  imasgim  40037  alephiso2  40250  isomushgr  44337  uspgrsprfo  44369
  Copyright terms: Public domain W3C validator