Theorem feq1 5621

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 5577	. . 3 |- ( F = G -> ( F Fn A <-> G Fn A ) )
2		rneq 5141	. . . 4 |- ( F = G -> ran F = ran G )
3	2	sseq1d 3444	. . 3 |- ( F = G -> ( ran F C_ B <-> ran G C_ B ) )
4	1, 3	anbi12d 708	. 2 |- ( F = G -> ( ( F Fn A /\ ran F C_ B ) <-> ( G Fn A /\ ran G C_ B ) ) )
5		df-f 5500	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
6		df-f 5500	. 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 367   = wceq 1399   C_ wss 3389   ran crn 4914   Fn wfn 5491   -->wf 5492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-fun 5498  df-fn 5499  df-f 5500

This theorem is referenced by:  feq1d  5625  feq1i  5631  elimf  5638  f00  5675  f0bi  5676  f0dom0  5677  fconstg  5680  f1eq1  5684  fconst2g  6028  fconstfvOLD  6035  elmapg  7351  ac6sfi  7679  ac5num  8330  acni2  8340  cofsmo  8562  cfsmolem  8563  cfcoflem  8565  coftr  8566  alephsing  8569  axdc2lem  8741  axdc3lem2  8744  axdc3lem3  8745  axdc3  8747  axdc4lem  8748  ac6num  8772  inar1  9064  1fv  11714  axdc4uzlem  11995  seqf1olem2  12050  seqf1o  12051  iswrd  12454  iswrdOLD  12455  wrdlen2i  12795  ramub2  14534  ramcl  14549  isacs2  15060  isacs1i  15064  mreacs  15065  mgmb1mgm1  16000  isgrpinv  16217  isghm  16384  islindf  18932  mat1dimelbas  19058  1stcfb  20031  upxp  20209  txcn  20212  isi1f  22166  mbfi1fseqlem6  22212  mbfi1flimlem  22214  itg2addlem  22250  plyf  22680  wlkelwrd  24651  iseupa  25086  isgrpo  25315  ismgmOLD  25439  elghomlem2OLD  25481  vci  25558  isvclem  25587  isnvlem  25620  ajmoi  25891  ajval  25894  hlimi  26222  chlimi  26269  chcompl  26277  adjmo  26867  adjeu  26924  adjval  26925  adj1  26968  adjeq  26970  cnlnssadj  27115  pjinvari  27226  padct  27695  locfinref  27998  isrnmeas  28327  fprb  29368  orderseqlem  29497  soseq  29499  elno  29571  volsupnfl  30224  mbfresfi  30226  filnetlem4  30365  upixp  30386  sdclem2  30401  sdclem1  30402  fdc  30404  ismrc  30799  fmuldfeqlem1  31742  fmuldfeq  31743  dvnprodlem1  31909  stoweidlem15  31963  stoweidlem16  31964  stoweidlem17  31965  stoweidlem19  31967  stoweidlem20  31968  stoweidlem21  31969  stoweidlem22  31970  stoweidlem23  31971  stoweidlem27  31975  stoweidlem31  31979  stoweidlem32  31980  stoweidlem42  31990  stoweidlem48  31996  stoweidlem51  31999  stoweidlem59  32007  lincdifsn  33225  bj-finsumval0  35010  istendo  36899