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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 5651 . . 3
21anbi1d 703 . 2
3 df-f 5573 . 2
4 df-f 5573 . 2
52, 3, 43bitr4g 288 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367   wceq 1405   wss 3414   crn 4824   wfn 5564  wf 5565 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380 This theorem depends on definitions:  df-bi 185  df-an 369  df-cleq 2394  df-fn 5572  df-f 5573 This theorem is referenced by:  feq23  5699  feq2d  5701  feq2i  5707  f00  5750  f0dom0  5752  f1eq2  5760  fressnfv  6065  fconstfvOLD  6115  mapvalg  7467  map0g  7496  ac6sfi  7798  cofsmo  8681  axcc4dom  8853  ac6sg  8900  isghm  16591  pjdm2  19040  cmpcovf  20184  ulmval  23067  measval  28646  isrnmeas  28648  poseq  30064  soseq  30065  elno2  30114  noreson  30120  noxpsgn  30125  nodenselem6  30146  bj-finsumval0  31227  mbfresfi  31433  stoweidlem62  37212
 Copyright terms: Public domain W3C validator