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

Theorem f1oeq3 5467
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 5436 . . 3  |-  ( A  =  B  ->  ( F : C -1-1-> A  <->  F : C -1-1-> B ) )
2 foeq3 5451 . . 3  |-  ( A  =  B  ->  ( F : C -onto-> A  <->  F : C -onto-> B ) )
31, 2anbi12d 691 . 2  |-  ( A  =  B  ->  (
( F : C -1-1-> A  /\  F : C -onto-> A )  <->  ( F : C -1-1-> B  /\  F : C -onto-> B ) ) )
4 df-f1o 5264 . 2  |-  ( F : C -1-1-onto-> A  <->  ( F : C -1-1-> A  /\  F : C -onto-> A ) )
5 df-f1o 5264 . 2  |-  ( F : C -1-1-onto-> B  <->  ( F : C -1-1-> B  /\  F : C -onto-> B ) )
63, 4, 53bitr4g 279 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 176    /\ wa 358    = wceq 1625   -1-1->wf1 5254   -onto->wfo 5255   -1-1-onto->wf1o 5256
This theorem is referenced by:  f1oeq23  5468  f1oeq123d  5471  f1ores  5489  resdif  5496  resin  5497  f1osng  5516  f1oprswap  5517  fveqf1o  5808  isoeq5  5822  isoini2  5838  ncanth  6297  oacomf1o  6565  mapsnf1o  6859  bren  6873  xpcomf1o  6953  domss2  7022  isinf  7078  wemapwe  7402  oef1o  7403  cnfcomlem  7404  cnfcom  7405  cnfcom2  7407  cnfcom3  7409  cnfcom3clem  7410  infxpenc  7647  infxpenc2lem1  7648  infxpenc2  7651  ackbij2lem2  7868  fin1a2lem6  8033  hsmexlem1  8054  pwfseqlem5  8287  pwfseq  8288  hashgf1o  11035  axdc4uzlem  11046  sumeq1f  12163  fsumss  12200  fsumcnv  12238  unbenlem  12957  4sqlem11  13004  pwssnf1o  13399  catcisolem  13940  yoniso  14061  xpsmnd  14414  gsumvalx  14453  gsumpropd  14455  xpsgrp  14616  cayley  14791  cayleyth  14792  gsumval3  15193  gsumcom2  15228  coe1mul2lem2  16347  cncfcnvcn  18426  ovolicc2lem4  18881  logf1o2  19999  adjbd1o  22667  rinvf1o  23040  gsumpropd2lem  23381  derangval  23700  subfacp1lem2a  23713  subfacp1lem3  23715  subfacp1lem5  23717  iseupa  23883  elgiso  24005  infemb  25870  ismtyval  26535  ismrer1  26573  rngoisoval  26619  pwfi2f1o  27271  imasgim  27275  lautset  30344  pautsetN  30360  hvmap1o2  32028
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264
  Copyright terms: Public domain W3C validator