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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 5495 . . 3
21anbi1d 704 . 2
3 df-f 5417 . 2
4 df-f 5417 . 2
52, 3, 43bitr4g 288 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1369   wss 3323   crn 4836   wfn 5408  wf 5409 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-12 1792  ax-ext 2419 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-fn 5416  df-f 5417 This theorem is referenced by:  feq23  5540  feq2d  5542  feq2i  5547  f00  5588  f0dom0  5590  f1eq2  5597  fressnfv  5891  fconstfv  5935  mapvalg  7216  map0g  7244  ac6sfi  7548  cofsmo  8430  axcc4dom  8602  ac6sg  8649  isghm  15738  pjdm2  18111  cmpcovf  18969  ulmval  21820  measval  26564  isrnmeas  26566  poseq  27665  soseq  27666  elno2  27746  noreson  27752  noxpsgn  27757  nodenselem6  27778  mbfresfi  28391  stoweidlem62  29810  bj-finsumval0  32426
 Copyright terms: Public domain W3C validator