MPE Home 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  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )

Proof of Theorem fneq2
StepHypRef Expression
1 eqeq2 2292 . . 3  |-  ( A  =  B  ->  ( dom  F  =  A  <->  dom  F  =  B ) )
21anbi2d 684 . 2  |-  ( A  =  B  ->  (
( Fun  F  /\  dom  F  =  A )  <-> 
( Fun  F  /\  dom  F  =  B ) ) )
3 df-fn 5258 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 df-fn 5258 . 2  |-  ( F  Fn  B  <->  ( Fun  F  /\  dom  F  =  B ) )
52, 3, 43bitr4g 279 1  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623   dom cdm 4689   Fun wfun 5249    Fn 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