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

Theorem f1oeq3 5481
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 5450 . . 3  |-  ( A  =  B  ->  ( F : C -1-1-> A  <->  F : C -1-1-> B ) )
2 foeq3 5465 . . 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 5278 . 2  |-  ( F : C -1-1-onto-> A  <->  ( F : C -1-1-> A  /\  F : C -onto-> A ) )
5 df-f1o 5278 . 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 1632   -1-1->wf1 5268   -onto->wfo 5269   -1-1-onto->wf1o 5270
This theorem is referenced by:  f1oeq23  5482  f1oeq123d  5485  f1ores  5503  resdif  5510  resin  5511  f1osng  5530  f1oprswap  5531  fveqf1o  5822  isoeq5  5836  isoini2  5852  ncanth  6311  oacomf1o  6579  mapsnf1o  6873  bren  6887  xpcomf1o  6967  domss2  7036  isinf  7092  wemapwe  7416  oef1o  7417  cnfcomlem  7418  cnfcom  7419  cnfcom2  7421  cnfcom3  7423  cnfcom3clem  7424  infxpenc  7661  infxpenc2lem1  7662  infxpenc2  7665  ackbij2lem2  7882  fin1a2lem6  8047  hsmexlem1  8068  pwfseqlem5  8301  pwfseq  8302  hashgf1o  11049  axdc4uzlem  11060  sumeq1f  12177  fsumss  12214  fsumcnv  12252  unbenlem  12971  4sqlem11  13018  pwssnf1o  13413  catcisolem  13954  yoniso  14075  xpsmnd  14428  gsumvalx  14467  gsumpropd  14469  xpsgrp  14630  cayley  14805  cayleyth  14806  gsumval3  15207  gsumcom2  15242  coe1mul2lem2  16361  cncfcnvcn  18440  ovolicc2lem4  18895  logf1o2  20013  adjbd1o  22681  rinvf1o  23054  gsumpropd2lem  23394  derangval  23713  subfacp1lem2a  23726  subfacp1lem3  23728  subfacp1lem5  23730  iseupa  23896  elgiso  24018  cprodeq1f  24130  infemb  25962  ismtyval  26627  ismrer1  26665  rngoisoval  26711  pwfi2f1o  27363  imasgim  27367  lautset  30893  pautsetN  30909  hvmap1o2  32577
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278
  Copyright terms: Public domain W3C validator