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.

Step	Hyp	Ref	Expression
1		f1oeq2 5813	. . 3
2		raleq 3054	. . . 4
3	2	raleqbi1dv 3062	. . 3
4	1, 3	anbi12d 710	. 2
5		df-isom 5602	. 2
6		df-isom 5602	. 2
7	4, 5, 6	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:  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