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

Theorem f1oeq3 5465
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 5434 . . 3  |-  ( A  =  B  ->  ( F : C -1-1-> A  <->  F : C -1-1-> B ) )
2 foeq3 5449 . . 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 5262 . 2  |-  ( F : C -1-1-onto-> A  <->  ( F : C -1-1-> A  /\  F : C -onto-> A ) )
5 df-f1o 5262 . 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 1623   -1-1->wf1 5252   -onto->wfo 5253   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1oeq23  5466  f1oeq123d  5469  f1ores  5487  resdif  5494  resin  5495  f1osng  5514  f1oprswap  5515  fveqf1o  5806  isoeq5  5820  isoini2  5836  ncanth  6295  oacomf1o  6563  mapsnf1o  6857  bren  6871  xpcomf1o  6951  domss2  7020  isinf  7076  wemapwe  7400  oef1o  7401  cnfcomlem  7402  cnfcom  7403  cnfcom2  7405  cnfcom3  7407  cnfcom3clem  7408  infxpenc  7645  infxpenc2lem1  7646  infxpenc2  7649  ackbij2lem2  7866  fin1a2lem6  8031  hsmexlem1  8052  pwfseqlem5  8285  pwfseq  8286  hashgf1o  11033  axdc4uzlem  11044  sumeq1f  12161  fsumss  12198  fsumcnv  12236  unbenlem  12955  4sqlem11  13002  pwssnf1o  13397  catcisolem  13938  yoniso  14059  xpsmnd  14412  gsumvalx  14451  gsumpropd  14453  xpsgrp  14614  cayley  14789  cayleyth  14790  gsumval3  15191  gsumcom2  15226  coe1mul2lem2  16345  cncfcnvcn  18424  ovolicc2lem4  18879  logf1o2  19997  adjbd1o  22665  rinvf1o  23038  gsumpropd2lem  23379  derangval  23698  subfacp1lem2a  23711  subfacp1lem3  23713  subfacp1lem5  23715  iseupa  23881  elgiso  24003  infemb  25859  ismtyval  26524  ismrer1  26562  rngoisoval  26608  pwfi2f1o  27260  imasgim  27264  lautset  30271  pautsetN  30287  hvmap1o2  31955
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262
  Copyright terms: Public domain W3C validator