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

Theorem f1oeq3 5669
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 5638 . . 3  |-  ( A  =  B  ->  ( F : C -1-1-> A  <->  F : C -1-1-> B ) )
2 foeq3 5653 . . 3  |-  ( A  =  B  ->  ( F : C -onto-> A  <->  F : C -onto-> B ) )
31, 2anbi12d 693 . 2  |-  ( A  =  B  ->  (
( F : C -1-1-> A  /\  F : C -onto-> A )  <->  ( F : C -1-1-> B  /\  F : C -onto-> B ) ) )
4 df-f1o 5463 . 2  |-  ( F : C -1-1-onto-> A  <->  ( F : C -1-1-> A  /\  F : C -onto-> A ) )
5 df-f1o 5463 . 2  |-  ( F : C -1-1-onto-> B  <->  ( F : C -1-1-> B  /\  F : C -onto-> B ) )
63, 4, 53bitr4g 281 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 178    /\ wa 360    = wceq 1653   -1-1->wf1 5453   -onto->wfo 5454   -1-1-onto->wf1o 5455
This theorem is referenced by:  f1oeq23  5670  f1oeq123d  5673  f1ores  5691  resdif  5698  resin  5699  f1osng  5718  fveqf1o  6031  isoeq5  6045  isoini2  6061  ncanth  6542  oacomf1o  6810  mapsnf1o  7105  bren  7119  xpcomf1o  7199  domss2  7268  isinf  7324  wemapwe  7656  oef1o  7657  cnfcomlem  7658  cnfcom2  7661  cnfcom3  7663  cnfcom3clem  7664  infxpenc  7901  infxpenc2lem1  7902  infxpenc2  7905  ackbij2lem2  8122  fin1a2lem6  8287  hsmexlem1  8308  pwfseqlem5  8540  pwfseq  8541  hashgf1o  11312  axdc4uzlem  11323  sumeq1f  12484  fsumss  12521  fsumcnv  12559  unbenlem  13278  4sqlem11  13325  pwssnf1o  13722  catcisolem  14263  yoniso  14384  xpsmnd  14737  gsumvalx  14776  gsumpropd  14778  xpsgrp  14939  cayley  15114  cayleyth  15115  gsumval3  15516  gsumcom2  15551  coe1mul2lem2  16663  cncfcnvcn  18953  ovolicc2lem4  19418  logf1o2  20543  iseupa  21689  adjbd1o  23590  rinvf1o  24044  gsumpropd2lem  24222  derangval  24855  subfacp1lem2a  24868  subfacp1lem3  24870  subfacp1lem5  24872  elgiso  25109  prodeq1f  25236  fprodss  25276  fprodcnv  25309  ismtyval  26511  ismrer1  26549  rngoisoval  26595  pwfi2f1o  27239  imasgim  27243  lautset  30941  pautsetN  30957  hvmap1o2  32625
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463
  Copyright terms: Public domain W3C validator