Theorem feq1 5545

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 5502	. . 3 |- ( F = G -> ( F Fn A <-> G Fn A ) )
2		rneq 5068	. . . 4 |- ( F = G -> ran F = ran G )
3	2	sseq1d 3386	. . 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 5425	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
6		df-f 5425	. 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 1369   C_ wss 3331   ran crn 4844   Fn wfn 5416   -->wf 5417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-br 4296  df-opab 4354  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-fun 5423  df-fn 5424  df-f 5425

This theorem is referenced by:  feq1d  5549  feq1i  5554  elimf  5561  f00  5596  f0bi  5597  f0dom0  5598  fconstg  5600  f1eq1  5604  fconst2g  5935  fconstfv  5943  elmapg  7230  ac6sfi  7559  ac5num  8209  acni2  8219  cofsmo  8441  cfsmolem  8442  cfcoflem  8444  coftr  8445  alephsing  8448  axdc2lem  8620  axdc3lem2  8623  axdc3lem3  8624  axdc3  8626  axdc4lem  8627  ac6num  8651  inar1  8945  1fv  11535  axdc4uzlem  11807  seqf1olem2  11849  seqf1o  11850  iswrd  12240  wrdlen2i  12549  ramub2  14078  ramcl  14093  isacs2  14594  isacs1i  14598  mreacs  14599  isgrpinv  15591  isghm  15750  islindf  18244  1stcfb  19052  upxp  19199  txcn  19202  isi1f  21155  mbfi1fseqlem6  21201  mbfi1flimlem  21203  itg2addlem  21239  plyf  21669  iseupa  23589  isgrpo  23686  ismgm  23810  elghomlem2  23852  vci  23929  isvclem  23958  isnvlem  23991  ajmoi  24262  ajval  24265  hlimi  24593  chlimi  24640  chcompl  24648  adjmo  25239  adjeu  25296  adjval  25297  adj1  25340  adjeq  25342  cnlnssadj  25487  pjinvari  25598  isrnmeas  26617  fprb  27587  orderseqlem  27716  soseq  27718  elno  27790  volsupnfl  28439  mbfresfi  28441  filnetlem4  28605  upixp  28626  sdclem2  28641  sdclem1  28642  fdc  28644  ismrc  29040  fmuldfeqlem1  29766  fmuldfeq  29767  stoweidlem15  29813  stoweidlem16  29814  stoweidlem17  29815  stoweidlem19  29817  stoweidlem20  29818  stoweidlem21  29819  stoweidlem22  29820  stoweidlem23  29821  stoweidlem27  29825  stoweidlem31  29829  stoweidlem32  29830  stoweidlem42  29840  stoweidlem48  29846  stoweidlem51  29849  stoweidlem59  29857  wlkelwrd  30283  mat1dimelbas  30870  lincdifsn  30961  bj-finsumval0  32586  istendo  34407