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

Theorem f1oeq3 5714
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq3

Proof of Theorem f1oeq3
StepHypRef Expression
1 f1eq3 5683 . . 3
2 foeq3 5698 . . 3
31, 2anbi12d 693 . 2
4 df-f1o 5508 . 2
5 df-f1o 5508 . 2
63, 4, 53bitr4g 281 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  =wceq 1654  -1-1->wf1 5498  -onto->wfo 5499  -1-1-onto->wf1o 5500
This theorem is referenced by:  f1oeq23  5715  f1oeq123d  5718  f1ores  5736  resdif  5743  resin  5744  f1osng  5763  fveqf1o  6077  isoeq5  6091  isoini2  6107  ncanth  6590  oacomf1o  6857  mapsnf1o  7152  bren  7166  xpcomf1o  7246  domss2  7315  isinf  7371  wemapwe  7703  oef1o  7704  cnfcomlem  7705  cnfcom2  7708  cnfcom3  7710  cnfcom3clem  7711  infxpenc  7950  infxpenc2lem1  7951  infxpenc2  7954  ackbij2lem2  8171  fin1a2lem6  8336  hsmexlem1  8357  pwfseqlem5  8589  pwfseq  8590  hashgf1o  11361  axdc4uzlem  11372  sumeq1f  12533  fsumss  12570  fsumcnv  12608  unbenlem  13327  4sqlem11  13374  pwssnf1o  13771  catcisolem  14312  yoniso  14433  xpsmnd  14786  gsumvalx  14825  gsumpropd  14827  xpsgrp  14988  cayley  15163  cayleyth  15164  gsumval3  15565  gsumcom2  15600  coe1mul2lem2  16712  cncfcnvcn  19002  ovolicc2lem4  19467  logf1o2  20592  iseupa  21738  adjbd1o  23639  rinvf1o  24090  gsumpropd2lem  24269  frabbijd  24722  eulerpartgbij  24758  eulerpartlemgh  24764  derangval  24957  subfacp1lem2a  24970  subfacp1lem3  24972  subfacp1lem5  24974  elgiso  25211  prodeq1f  25338  fprodss  25378  fprodcnv  25411  ismtyval  26620  ismrer1  26658  rngoisoval  26704  pwfi2f1o  27416  imasgim  27420  lautset  31119  pautsetN  31135  hvmap1o2  32803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3316  df-ss 3323  df-f 5505  df-f1 5506  df-fo 5507  df-f1o 5508
  Copyright terms: Public domain W3C validator