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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 5564 . . 3
21anbi1d 687 . 2
3 df-f 5487 . 2
4 df-f 5487 . 2
52, 3, 43bitr4g 281 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   wceq 1653   wss 3306   crn 4908   wfn 5478  wf 5479 This theorem is referenced by:  feq23  5608  feq2d  5610  feq2i  5615  f00  5657  f1eq2  5664  fressnfv  5949  fconstfv  5983  mapvalg  7057  map0g  7082  ac6sfi  7380  cofsmo  8180  axcc4dom  8352  ac6sg  8399  isghm  15037  pjdm2  16969  cmpcovf  17485  ulmval  20327  measval  24583  isrnmeas  24585  poseq  25559  soseq  25560  elno2  25640  noreson  25646  noxpsgn  25651  nodenselem6  25672  mbfresfi  26289  stoweidlem62  27825 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-11 1763  ax-ext 2423 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2435  df-fn 5486  df-f 5487
 Copyright terms: Public domain W3C validator