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

Theorem fneq2 5334
 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 2292 . . 3
21anbi2d 684 . 2
3 df-fn 5258 . 2
4 df-fn 5258 . 2
52, 3, 43bitr4g 279 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   wceq 1623   cdm 4689   wfun 5249   wfn 5250 This theorem is referenced by:  fneq2d  5336  fneq2i  5339  feq2  5376  foeq2  5448  f1o00  5508  eqfnfv2  5623  fconstfv  5734  tfrlem3  6393  tfrlem12  6405  ixpeq1  6827  ac5  8104  0fz1  10813  wfrlem1  24256  wfrlem15  24270  frrlem1  24281  bpolyval  24784  ac5g  25075  fnchoice  27700  bnj90  28748  bnj919  28797  bnj535  28922  bnj1463  29085 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264 This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276  df-fn 5258
 Copyright terms: Public domain W3C validator