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

Theorem fneq2 5679
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 2437 . . 3  |-  ( A  =  B  ->  ( dom  F  =  A  <->  dom  F  =  B ) )
21anbi2d 708 . 2  |-  ( A  =  B  ->  (
( Fun  F  /\  dom  F  =  A )  <-> 
( Fun  F  /\  dom  F  =  B ) ) )
3 df-fn 5600 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 df-fn 5600 . 2  |-  ( F  Fn  B  <->  ( Fun  F  /\  dom  F  =  B ) )
52, 3, 43bitr4g 291 1  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   dom cdm 4849   Fun wfun 5591    Fn wfn 5592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2414  df-fn 5600
This theorem is referenced by:  fneq2d  5681  fneq2i  5685  feq2  5725  foeq2  5803  f1o00  5859  eqfnfv2  5988  fconstfvOLD  6138  wfrlem1  7039  wfrlem15  7054  tfrlem12  7111  ixpeq1  7537  ac5  8907  0fz1  11819  esumcvgsum  28904  bnj90  29523  bnj919  29573  bnj535  29696  bnj1463  29859  frrlem1  30508  fnchoice  37210
  Copyright terms: Public domain W3C validator