Theorem feq1 5704

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 5660	. . 3 |- ( F = G -> ( F Fn A <-> G Fn A ) )
2		rneq 5219	. . . 4 |- ( F = G -> ran F = ran G )
3	2	sseq1d 3524	. . 3 |- ( F = G -> ( ran F C_ B <-> ran G C_ B ) )
4	1, 3	anbi12d 710	. 2 |- ( F = G -> ( ( F Fn A /\ ran F C_ B ) <-> ( G Fn A /\ ran G C_ B ) ) )
5		df-f 5583	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
6		df-f 5583	. 2 |- ( G : A --> B <-> ( G Fn A /\ ran G C_ B ) )
7	4, 5, 6	3bitr4g 288	1 |- ( F = G -> ( F : A --> B <-> G : A --> B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1374   C_ wss 3469   ran crn 4993   Fn wfn 5574   -->wf 5575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-fun 5581  df-fn 5582  df-f 5583

This theorem is referenced by:  feq1d  5708  feq1i  5714  elimf  5721  f00  5758  f0bi  5759  f0dom0  5760  fconstg  5763  f1eq1  5767  fconst2g  6106  fconstfv  6114  elmapg  7423  ac6sfi  7753  ac5num  8406  acni2  8416  cofsmo  8638  cfsmolem  8639  cfcoflem  8641  coftr  8642  alephsing  8645  axdc2lem  8817  axdc3lem2  8820  axdc3lem3  8821  axdc3  8823  axdc4lem  8824  ac6num  8848  inar1  9142  1fv  11778  axdc4uzlem  12048  seqf1olem2  12103  seqf1o  12104  iswrd  12503  wrdlen2i  12834  ramub2  14380  ramcl  14395  isacs2  14897  isacs1i  14901  mreacs  14902  isgrpinv  15894  isghm  16055  islindf  18607  mat1dimelbas  18733  1stcfb  19705  upxp  19852  txcn  19855  isi1f  21809  mbfi1fseqlem6  21855  mbfi1flimlem  21857  itg2addlem  21893  plyf  22323  wlkelwrd  24192  iseupa  24627  isgrpo  24860  ismgm  24984  elghomlem2  25026  vci  25103  isvclem  25132  isnvlem  25165  ajmoi  25436  ajval  25439  hlimi  25767  chlimi  25814  chcompl  25822  adjmo  26413  adjeu  26470  adjval  26471  adj1  26514  adjeq  26516  cnlnssadj  26661  pjinvari  26772  isrnmeas  27797  fprb  28766  orderseqlem  28895  soseq  28897  elno  28969  volsupnfl  29623  mbfresfi  29625  filnetlem4  29789  upixp  29810  sdclem2  29825  sdclem1  29826  fdc  29828  ismrc  30224  fmuldfeqlem1  31087  fmuldfeq  31088  stoweidlem15  31270  stoweidlem16  31271  stoweidlem17  31272  stoweidlem19  31274  stoweidlem20  31275  stoweidlem21  31276  stoweidlem22  31277  stoweidlem23  31278  stoweidlem27  31282  stoweidlem31  31286  stoweidlem32  31287  stoweidlem42  31297  stoweidlem48  31303  stoweidlem51  31306  stoweidlem59  31314  fourierdlem60  31422  fourierdlem61  31423  fourierdlem80  31442  lincdifsn  31973  bj-finsumval0  33610  istendo  35431