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

Theorem isoeq5 6219
 Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
Assertion
Ref Expression
isoeq5

Proof of Theorem isoeq5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oeq3 5814 . . 3
21anbi1d 704 . 2
3 df-isom 5602 . 2
4 df-isom 5602 . 2
52, 3, 43bitr4g 288 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  A.wral 2807   class class class wbr 4452  -1-1-onto->wf1o 5592  cfv 5593  Isom`wiso 5594 This theorem is referenced by:  isores3  6231  ordiso  7962  ordtypelem9  7972  ordtypelem10  7973  oiid  7987  iunfictbso  8516  ltweuz  12072  fz1isolem  12510  dvgt0lem2  22404  erdszelem1  28635  erdsze  28646  erdsze2lem1  28647  erdsze2lem2  28648  fourierdlem50  31939  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem100  31989  fourierdlem108  31997  fourierdlem110  31999  fourierdlem112  32001  fourierdlem113  32002 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-isom 5602
 Copyright terms: Public domain W3C validator