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

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

Proof of Theorem isoeq4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oeq2 5813 . . 3
2 raleq 3054 . . . 4
32raleqbi1dv 3062 . . 3
41, 3anbi12d 710 . 2
5 df-isom 5602 . 2
6 df-isom 5602 . 2
74, 5, 63bitr4g 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:  oieu  7985  oiid  7987  finnisoeu  8515  iunfictbso  8516  fz1isolem  12510  isercolllem3  13489  summolem2a  13537  prodmolem2a  13741  erdszelem1  28635  erdsze  28646  erdsze2lem1  28647  erdsze2lem2  28648  fzisoeu  31500  fourierdlem36  31925  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-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-isom 5602
 Copyright terms: Public domain W3C validator