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

Theorem f1oeq3 6433
 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 6399 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶1-1𝐴𝐹:𝐶1-1𝐵))
2 foeq3 6415 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
31, 2anbi12d 622 . 2 (𝐴 = 𝐵 → ((𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴) ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵)))
4 df-f1o 6193 . 2 (𝐹:𝐶1-1-onto𝐴 ↔ (𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴))
5 df-f1o 6193 . 2 (𝐹:𝐶1-1-onto𝐵 ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵))
63, 4, 53bitr4g 306 1 (𝐴 = 𝐵 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1508  –1-1→wf1 6183  –onto→wfo 6184  –1-1-onto→wf1o 6185 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-in 3831  df-ss 3838  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193 This theorem is referenced by:  f1oeq23  6434  f1oeq123d  6437  f1oeq3d  6439  f1ores  6456  resin  6463  isoeq5  6896  ncanth  6934  bren  8314  xpcomf1o  8401  isinf  8525  cnfcom2  8958  fin1a2lem6  9624  pwfseqlem5  9882  pwfseq  9883  hashgf1o  13153  axdc4uzlem  13165  sumeq1  14905  prodeq1f  15121  unbenlem  16099  4sqlem11  16146  gsumvalx  17751  cayley  18316  cayleyth  18317  ovolicc2lem4  23840  logf1o2  24950  uspgrf1oedg  26677  wlkiswwlks2lem4  27374  clwwlknonclwlknonf1o  27926  clwwlknonclwlknonf1oOLD  27927  dlwwlknondlwlknonf1o  27932  dlwwlknondlwlknonf1oOLD  27933  adjbd1o  29659  rinvf1o  30156  eulerpartgbij  31308  eulerpartlemgh  31314  derangval  32032  subfacp1lem2a  32045  subfacp1lem3  32047  subfacp1lem5  32049  mrsubff1o  32315  msubff1o  32357  bj-finsumval0  34063  f1omptsnlem  34092  f1omptsn  34093  poimirlem4  34370  poimirlem9  34375  poimirlem15  34381  ismtyval  34553  ismrer1  34591  lautset  36696  pautsetN  36712  hvmap1o2  38379  pwfi2f1o  39126  imasgim  39130  isomushgr  43389  uspgrsprfo  43421
 Copyright terms: Public domain W3C validator