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

Theorem f1oeq3 5659
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq3  |-  ( A  =  B  ->  ( F : C -1-1-onto-> A  <->  F : C -1-1-onto-> B ) )

Proof of Theorem f1oeq3
StepHypRef Expression
1 f1eq3 5628 . . 3  |-  ( A  =  B  ->  ( F : C -1-1-> A  <->  F : C -1-1-> B ) )
2 foeq3 5643 . . 3  |-  ( A  =  B  ->  ( F : C -onto-> A  <->  F : C -onto-> B ) )
31, 2anbi12d 692 . 2  |-  ( A  =  B  ->  (
( F : C -1-1-> A  /\  F : C -onto-> A )  <->  ( F : C -1-1-> B  /\  F : C -onto-> B ) ) )
4 df-f1o 5453 . 2  |-  ( F : C -1-1-onto-> A  <->  ( F : C -1-1-> A  /\  F : C -onto-> A ) )
5 df-f1o 5453 . 2  |-  ( F : C -1-1-onto-> B  <->  ( F : C -1-1-> B  /\  F : C -onto-> B ) )
63, 4, 53bitr4g 280 1  |-  ( A  =  B  ->  ( F : C -1-1-onto-> A  <->  F : C -1-1-onto-> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652   -1-1->wf1 5443   -onto->wfo 5444   -1-1-onto->wf1o 5445
This theorem is referenced by:  f1oeq23  5660  f1oeq123d  5663  f1ores  5681  resdif  5688  resin  5689  f1osng  5708  fveqf1o  6021  isoeq5  6035  isoini2  6051  ncanth  6532  oacomf1o  6800  mapsnf1o  7095  bren  7109  xpcomf1o  7189  domss2  7258  isinf  7314  wemapwe  7646  oef1o  7647  cnfcomlem  7648  cnfcom2  7651  cnfcom3  7653  cnfcom3clem  7654  infxpenc  7891  infxpenc2lem1  7892  infxpenc2  7895  ackbij2lem2  8112  fin1a2lem6  8277  hsmexlem1  8298  pwfseqlem5  8530  pwfseq  8531  hashgf1o  11302  axdc4uzlem  11313  sumeq1f  12474  fsumss  12511  fsumcnv  12549  unbenlem  13268  4sqlem11  13315  pwssnf1o  13712  catcisolem  14253  yoniso  14374  xpsmnd  14727  gsumvalx  14766  gsumpropd  14768  xpsgrp  14929  cayley  15104  cayleyth  15105  gsumval3  15506  gsumcom2  15541  coe1mul2lem2  16653  cncfcnvcn  18943  ovolicc2lem4  19408  logf1o2  20533  iseupa  21679  adjbd1o  23580  rinvf1o  24034  gsumpropd2lem  24212  derangval  24845  subfacp1lem2a  24858  subfacp1lem3  24860  subfacp1lem5  24862  elgiso  25099  prodeq1f  25226  fprodss  25266  fprodcnv  25299  ismtyval  26500  ismrer1  26538  rngoisoval  26584  pwfi2f1o  27228  imasgim  27232  lautset  30816  pautsetN  30832  hvmap1o2  32500
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453
  Copyright terms: Public domain W3C validator