MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq1 Unicode version

Theorem feq1 5718
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
feq1

Proof of Theorem feq1
StepHypRef Expression
1 fneq1 5674 . . 3
2 rneq 5233 . . . 4
32sseq1d 3530 . . 3
41, 3anbi12d 710 . 2
5 df-f 5597 . 2
6 df-f 5597 . 2
74, 5, 63bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  C_wss 3475  rancrn 5005  Fnwfn 5588  -->wf 5589
This theorem is referenced by:  feq1d  5722  feq1i  5728  elimf  5735  f00  5772  f0bi  5773  f0dom0  5774  fconstg  5777  f1eq1  5781  fconst2g  6125  fconstfvOLD  6134  elmapg  7452  ac6sfi  7784  ac5num  8438  acni2  8448  cofsmo  8670  cfsmolem  8671  cfcoflem  8673  coftr  8674  alephsing  8677  axdc2lem  8849  axdc3lem2  8852  axdc3lem3  8853  axdc3  8855  axdc4lem  8856  ac6num  8880  inar1  9174  1fv  11821  axdc4uzlem  12092  seqf1olem2  12147  seqf1o  12148  iswrd  12550  wrdlen2i  12884  ramub2  14532  ramcl  14547  isacs2  15050  isacs1i  15054  mreacs  15055  mgmb1mgm1  15883  isgrpinv  16100  isghm  16267  islindf  18847  mat1dimelbas  18973  1stcfb  19946  upxp  20124  txcn  20127  isi1f  22081  mbfi1fseqlem6  22127  mbfi1flimlem  22129  itg2addlem  22165  plyf  22595  wlkelwrd  24530  iseupa  24965  isgrpo  25198  ismgmOLD  25322  elghomlem2OLD  25364  vci  25441  isvclem  25470  isnvlem  25503  ajmoi  25774  ajval  25777  hlimi  26105  chlimi  26152  chcompl  26160  adjmo  26751  adjeu  26808  adjval  26809  adj1  26852  adjeq  26854  cnlnssadj  26999  pjinvari  27110  locfinref  27844  isrnmeas  28171  fprb  29203  orderseqlem  29332  soseq  29334  elno  29406  volsupnfl  30059  mbfresfi  30061  filnetlem4  30199  upixp  30220  sdclem2  30235  sdclem1  30236  fdc  30238  ismrc  30633  fmuldfeqlem1  31576  fmuldfeq  31577  dvnprodlem1  31743  stoweidlem15  31797  stoweidlem16  31798  stoweidlem17  31799  stoweidlem19  31801  stoweidlem20  31802  stoweidlem21  31803  stoweidlem22  31804  stoweidlem23  31805  stoweidlem27  31809  stoweidlem31  31813  stoweidlem32  31814  stoweidlem42  31824  stoweidlem48  31830  stoweidlem51  31833  stoweidlem59  31841  lincdifsn  33025  bj-finsumval0  34663  istendo  36486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-fun 5595  df-fn 5596  df-f 5597
  Copyright terms: Public domain W3C validator