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

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

Proof of Theorem f1oeq1
StepHypRef Expression
1 f1eq1 5681 . . 3
2 foeq1 5696 . . 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:  f1oeq123d  5718  f1ocnvb  5735  f1orescnv  5737  resin  5744  f1ovi  5761  f1osng  5763  fsn  5954  fveqf1o  6077  isoeq1  6087  oacomf1o  6857  mapsn  7104  mapsnf1o3  7111  f1oen3g  7172  ensn1  7220  xpcomf1o  7246  omf1o  7260  domss2  7315  php3  7342  isinf  7371  ssfi  7378  oef1o  7704  cnfcomlem  7705  cnfcom  7706  cnfcom2  7708  cnfcom3  7710  cnfcom3clem  7711  infxpenc  7950  infxpenc2lem2  7952  infxpenc2  7954  ackbij2lem2  8171  ackbij2  8174  canthp1lem2  8579  pwfseqlem5  8589  pwfseq  8590  seqf1olem2  11414  seqf1o  11415  hasheqf1oi  11686  hashf1rn  11687  hashfacen  11754  summo  12562  fsum  12565  ackbijnn  12658  bitsf1ocnv  13007  sadcaddlem  13020  unbenlem  13327  setcinv  14296  yonffthlem  14430  grplactcnv  14938  eqgen  15044  isgim  15100  elsymgbas2  15147  cayleyth  15164  gsumval3eu  15564  gsumval3  15565  islmim  16185  coe1mul2lem2  16712  znunithash  16896  tgpconcompeqg  18192  resinf1o  20489  efif1olem4  20498  logf1o  20513  relogf1o  20515  dvlog  20593  nbgraf1o0  21507  cusgrafilem3  21541  iseupa  21738  eupares  21748  eupap1  21749  hoif  23308  indf1o  24470  fcobijfs  24721  frabbijd  24722  fpwrelmapffs  24738  eulerpartlem1  24753  eulerpartgbij  24758  eulerpart  24768  derangenlem  24961  subfacp1lem2a  24970  subfacp1lem3  24972  subfacp1lem5  24974  subfacp1lem6  24975  subfacp1  24976  elgiso  25211  prodmo  25366  fprod  25371  isismty  26621  ismrer1  26658  isrngoiso  26705  eldioph2lem1  26999  enfixsn  27413  pwfi2f1o  27416  frgrancvvdeqlem9  28668  islaut  31120  ispautN  31136  hvmap1o  32801
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-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2721  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3766  df-sn 3847  df-pr 3848  df-op 3850  df-br 4244  df-opab 4302  df-rel 4926  df-cnv 4927  df-co 4928  df-dm 4929  df-rn 4930  df-fun 5503  df-fn 5504  df-f 5505  df-f1 5506  df-fo 5507  df-f1o 5508
  Copyright terms: Public domain W3C validator