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

Theorem fneq2 5675
Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fneq2

Proof of Theorem fneq2
StepHypRef Expression
1 eqeq2 2472 . . 3
21anbi2d 703 . 2
3 df-fn 5596 . 2
4 df-fn 5596 . 2
52, 3, 43bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  domcdm 5004  Funwfun 5587  Fnwfn 5588
This theorem is referenced by:  fneq2d  5677  fneq2i  5681  feq2  5719  foeq2  5797  f1o00  5853  eqfnfv2  5982  fconstfvOLD  6134  tfrlem12  7077  ixpeq1  7500  ac5  8878  0fz1  11734  wfrlem1  29343  wfrlem15  29357  frrlem1  29387  fnchoice  31404  bnj90  33775  bnj919  33825  bnj535  33948  bnj1463  34111
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-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-fn 5596
  Copyright terms: Public domain W3C validator