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

Theorem f1oeq3 5607
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 5576 . . 3  |-  ( A  =  B  ->  ( F : C -1-1-> A  <->  F : C -1-1-> B ) )
2 foeq3 5591 . . 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 5401 . 2  |-  ( F : C -1-1-onto-> A  <->  ( F : C -1-1-> A  /\  F : C -onto-> A ) )
5 df-f1o 5401 . 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 1649   -1-1->wf1 5391   -onto->wfo 5392   -1-1-onto->wf1o 5393
This theorem is referenced by:  f1oeq23  5608  f1oeq123d  5611  f1ores  5629  resdif  5636  resin  5637  f1osng  5656  fveqf1o  5968  isoeq5  5982  isoini2  5998  ncanth  6476  oacomf1o  6744  mapsnf1o  7039  bren  7053  xpcomf1o  7133  domss2  7202  isinf  7258  wemapwe  7587  oef1o  7588  cnfcomlem  7589  cnfcom2  7592  cnfcom3  7594  cnfcom3clem  7595  infxpenc  7832  infxpenc2lem1  7833  infxpenc2  7836  ackbij2lem2  8053  fin1a2lem6  8218  hsmexlem1  8239  pwfseqlem5  8471  pwfseq  8472  hashgf1o  11237  axdc4uzlem  11248  sumeq1f  12409  fsumss  12446  fsumcnv  12484  unbenlem  13203  4sqlem11  13250  pwssnf1o  13647  catcisolem  14188  yoniso  14309  xpsmnd  14662  gsumvalx  14701  gsumpropd  14703  xpsgrp  14864  cayley  15039  cayleyth  15040  gsumval3  15441  gsumcom2  15476  coe1mul2lem2  16588  cncfcnvcn  18822  ovolicc2lem4  19283  logf1o2  20408  iseupa  21535  adjbd1o  23436  rinvf1o  23885  gsumpropd2lem  24049  derangval  24632  subfacp1lem2a  24645  subfacp1lem3  24647  subfacp1lem5  24649  elgiso  24886  prodeq1f  25013  fprodss  25053  ismtyval  26200  ismrer1  26238  rngoisoval  26284  pwfi2f1o  26929  imasgim  26933  lautset  30196  pautsetN  30212  hvmap1o2  31880
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-in 3270  df-ss 3277  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401
  Copyright terms: Public domain W3C validator