Theorem feq3 5720

Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
feq3

Proof of Theorem feq3

Step	Hyp	Ref	Expression
1		sseq2 3525	. . 3
2	1	anbi2d 703	. 2
3		df-f 5597	. 2
4		df-f 5597	. 2
5	2, 3, 4	3bitr4g 288	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  C_wss 3475  rancrn 5005  Fnwfn 5588  -->wf 5589

This theorem is referenced by:  feq23  5721  feq3d  5724  fun2  5754  fconstg  5777  f1eq3  5783  mapvalg  7449  mapsn  7480  cantnff  8114  axdc4uz  12093  supcvg  13667  gsumzsubmclOLD  16929  lmff  19802  txcn  20127  lmmbr  21697  iscmet3  21732  dvcnvrelem2  22419  itgsubstlem  22449  isumgra  24315  wlks  24519  wlkcompim  24526  wlkelwrd  24530  iseupa  24965  isgrpo  25198  vci  25441  isvclem  25470  vcoprnelem  25471  nmop0h  26910  cvmliftlem15  28743  mtyf  28912  ghomgrpilem2  29026  sdclem1  30236  stoweidlem57  31839  uhgrepe  32378

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