Theorem feq1 5539

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 5496	. . 3 |- ( F = G -> ( F Fn A <-> G Fn A ) )
2		rneq 5061	. . . 4 |- ( F = G -> ran F = ran G )
3	2	sseq1d 3380	. . 3 |- ( F = G -> ( ran F C_ B <-> ran G C_ B ) )
4	1, 3	anbi12d 705	. 2 |- ( F = G -> ( ( F Fn A /\ ran F C_ B ) <-> ( G Fn A /\ ran G C_ B ) ) )
5		df-f 5419	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
6		df-f 5419	. 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 1364   C_ wss 3325   ran crn 4837   Fn wfn 5410   -->wf 5411

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 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-fun 5417  df-fn 5418  df-f 5419

This theorem is referenced by:  feq1d  5543  feq1i  5548  elimf  5555  f00  5590  f0bi  5591  f0dom0  5592  fconstg  5594  f1eq1  5598  fconst2g  5929  fconstfv  5937  elmapg  7223  ac6sfi  7552  ac5num  8202  acni2  8212  cofsmo  8434  cfsmolem  8435  cfcoflem  8437  coftr  8438  alephsing  8441  axdc2lem  8613  axdc3lem2  8616  axdc3lem3  8617  axdc3  8619  axdc4lem  8620  ac6num  8644  inar1  8938  1fv  11528  axdc4uzlem  11800  seqf1olem2  11842  seqf1o  11843  iswrd  12233  wrdlen2i  12542  ramub2  14071  ramcl  14086  isacs2  14587  isacs1i  14591  mreacs  14592  isgrpinv  15581  isghm  15740  islindf  18200  1stcfb  19008  upxp  19155  txcn  19158  isi1f  21111  mbfi1fseqlem6  21157  mbfi1flimlem  21159  itg2addlem  21195  plyf  21625  iseupa  23521  isgrpo  23618  ismgm  23742  elghomlem2  23784  vci  23861  isvclem  23890  isnvlem  23923  ajmoi  24194  ajval  24197  hlimi  24525  chlimi  24572  chcompl  24580  adjmo  25171  adjeu  25228  adjval  25229  adj1  25272  adjeq  25274  cnlnssadj  25419  pjinvari  25530  isrnmeas  26550  fprb  27513  orderseqlem  27642  soseq  27644  elno  27716  volsupnfl  28361  mbfresfi  28363  filnetlem4  28527  upixp  28548  sdclem2  28563  sdclem1  28564  fdc  28566  ismrc  28962  fmuldfeqlem1  29688  fmuldfeq  29689  stoweidlem15  29735  stoweidlem16  29736  stoweidlem17  29737  stoweidlem19  29739  stoweidlem20  29740  stoweidlem21  29741  stoweidlem22  29742  stoweidlem23  29743  stoweidlem27  29747  stoweidlem31  29751  stoweidlem32  29752  stoweidlem42  29762  stoweidlem48  29768  stoweidlem51  29771  stoweidlem59  29779  wlkelwrd  30205  mat1dimelbas  30750  lincdifsn  30799  bj-finsumval0  32308  istendo  34126