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.

Step	Hyp	Ref	Expression
1		f1oeq3 5814	. . 3
2	1	anbi1d 704	. 2
3		df-isom 5602	. 2
4		df-isom 5602	. 2
5	2, 3, 4	3bitr4g 288	1

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  Isomwiso 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