Theorem feq1 5535

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

Assertion

Ref	Expression
feq1	|- ( F = G -> ( F : A --> B <-> G : A --> B ) )

Proof of Theorem feq1

Step	Hyp	Ref	Expression
1		fneq1 5493	. . 3 |- ( F = G -> ( F Fn A <-> G Fn A ) )
2		rneq 5054	. . . 4 |- ( F = G -> ran F = ran G )
3	2	sseq1d 3335	. . 3 |- ( F = G -> ( ran F C_ B <-> ran G C_ B ) )
4	1, 3	anbi12d 692	. 2 |- ( F = G -> ( ( F Fn A /\ ran F C_ B ) <-> ( G Fn A /\ ran G C_ B ) ) )
5		df-f 5417	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
6		df-f 5417	. 2 |- ( G : A --> B <-> ( G Fn A /\ ran G C_ B ) )
7	4, 5, 6	3bitr4g 280	1 |- ( F = G -> ( F : A --> B <-> G : A --> B ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   C_ wss 3280   ran crn 4838   Fn wfn 5408   -->wf 5409

This theorem is referenced by:  feq1d  5539  feq1i  5544  elimf  5549  f00  5587  fconstg  5589  f1eq1  5593  fconst2g  5905  fconstfv  5913  elmapg  6990  ac6sfi  7310  ac5num  7873  acni2  7883  cofsmo  8105  cfsmolem  8106  cfcoflem  8108  coftr  8109  alephsing  8112  axdc2lem  8284  axdc3lem2  8287  axdc3lem3  8288  axdc3  8290  axdc4lem  8291  ac6num  8315  inar1  8606  1fv  11075  axdc4uzlem  11276  seqf1olem2  11318  seqf1o  11319  iswrd  11684  ramub2  13337  ramcl  13352  isacs2  13833  isacs1i  13837  mreacs  13838  isgrpinv  14810  isghm  14961  1stcfb  17461  upxp  17608  txcn  17611  isi1f  19519  mbfi1fseqlem6  19565  mbfi1flimlem  19567  itg2addlem  19603  plyf  20070  iseupa  21640  isgrpo  21737  ismgm  21861  elghomlem2  21903  vci  21980  isvclem  22009  isnvlem  22042  ajmoi  22313  ajval  22316  hlimi  22643  chlimi  22690  chcompl  22698  adjmo  23288  adjeu  23345  adjval  23346  adj1  23389  adjeq  23391  cnlnssadj  23536  pjinvari  23647  isrnmeas  24507  fprb  25343  orderseqlem  25466  soseq  25468  elno  25514  volsupnfl  26150  mbfresfi  26152  filnetlem4  26300  upixp  26321  sdclem2  26336  sdclem1  26337  fdc  26339  ismrc  26645  islindf  27150  fmuldfeqlem1  27579  fmuldfeq  27580  stoweidlem15  27631  stoweidlem16  27632  stoweidlem17  27633  stoweidlem19  27635  stoweidlem20  27636  stoweidlem21  27637  stoweidlem22  27638  stoweidlem23  27639  stoweidlem27  27643  stoweidlem31  27647  stoweidlem32  27648  stoweidlem42  27658  stoweidlem48  27664  stoweidlem51  27667  stoweidlem59  27675  istendo  31242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-fun 5415  df-fn 5416  df-f 5417