Theorem feq1 5732

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 5686	. . 3 |- ( F = G -> ( F Fn A <-> G Fn A ) )
2		rneq 5079	. . . 4 |- ( F = G -> ran F = ran G )
3	2	sseq1d 3471	. . 3 |- ( F = G -> ( ran F C_ B <-> ran G C_ B ) )
4	1, 3	anbi12d 722	. 2 |- ( F = G -> ( ( F Fn A /\ ran F C_ B ) <-> ( G Fn A /\ ran G C_ B ) ) )
5		df-f 5605	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
6		df-f 5605	. 2 |- ( G : A --> B <-> ( G Fn A /\ ran G C_ B ) )
7	4, 5, 6	3bitr4g 296	1 |- ( F = G -> ( F : A --> B <-> G : A --> B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   C_ wss 3416   ran crn 4854   Fn wfn 5596   -->wf 5597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-opab 4476  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-fun 5603  df-fn 5604  df-f 5605

This theorem is referenced by:  feq1d  5736  feq1i  5742  elimf  5750  f00  5788  f0bi  5789  f0dom0  5790  fconstg  5793  f1eq1  5797  fconst2g  6143  fconstfvOLD  6152  fsnex  6206  elmapg  7511  ac6sfi  7841  ac5num  8493  acni2  8503  cofsmo  8725  cfsmolem  8726  cfcoflem  8728  coftr  8729  alephsing  8732  axdc2lem  8904  axdc3lem2  8907  axdc3lem3  8908  axdc3  8910  axdc4lem  8911  ac6num  8935  inar1  9226  1fv  11939  axdc4uzlem  12227  seqf1olem2  12285  seqf1o  12286  iswrd  12705  iswrdOLD  12706  wrdlen2i  13067  ramub2  15020  ramcl  15036  isacs2  15608  isacs1i  15612  mreacs  15613  mgmb1mgm1  16548  isgrpinv  16765  isghm  16932  islindf  19419  mat1dimelbas  19545  1stcfb  20509  upxp  20687  txcn  20690  isi1f  22681  mbfi1fseqlem6  22727  mbfi1flimlem  22729  itg2addlem  22765  plyf  23201  wlkelwrd  25307  iseupa  25742  isgrpo  25973  ismgmOLD  26097  elghomlem2OLD  26139  vci  26216  isvclem  26245  isnvlem  26278  ajmoi  26549  ajval  26552  hlimi  26890  chlimi  26936  chcompl  26944  adjmo  27534  adjeu  27591  adjval  27592  adj1  27635  adjeq  27637  cnlnssadj  27782  pjinvari  27893  padct  28356  locfinref  28717  isrnmeas  29071  fprb  30462  orderseqlem  30539  soseq  30541  elno  30582  filnetlem4  31086  bj-finsumval0  31747  poimirlem25  32010  poimirlem28  32013  volsupnfl  32030  mbfresfi  32032  upixp  32101  sdclem2  32116  sdclem1  32117  fdc  32119  istendo  34372  ismrc  35588  fmuldfeqlem1  37698  fmuldfeq  37699  dvnprodlem1  37859  stoweidlem15  37913  stoweidlem16  37914  stoweidlem17  37915  stoweidlem19  37917  stoweidlem20  37918  stoweidlem21  37919  stoweidlem22  37920  stoweidlem23  37921  stoweidlem27  37925  stoweidlem31  37930  stoweidlem32  37931  stoweidlem42  37941  stoweidlem48  37947  stoweidlem51  37950  stoweidlem59  37958  isomenndlem  38389  griedg0prc  39386  lincdifsn  40490