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

Theorem fneq2 5676
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 2482 . . 3  |-  ( A  =  B  ->  ( dom  F  =  A  <->  dom  F  =  B ) )
21anbi2d 703 . 2  |-  ( A  =  B  ->  (
( Fun  F  /\  dom  F  =  A )  <-> 
( Fun  F  /\  dom  F  =  B ) ) )
3 df-fn 5597 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 df-fn 5597 . 2  |-  ( F  Fn  B  <->  ( Fun  F  /\  dom  F  =  B ) )
52, 3, 43bitr4g 288 1  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   dom cdm 5005   Fun wfun 5588    Fn wfn 5589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fn 5597
This theorem is referenced by:  fneq2d  5678  fneq2i  5682  feq2  5720  foeq2  5798  f1o00  5854  eqfnfv2  5983  fconstfv  6134  tfrlem12  7070  ixpeq1  7492  ac5  8869  0fz1  11717  wfrlem1  29261  wfrlem15  29275  frrlem1  29305  fnchoice  31297  bnj90  33211  bnj919  33260  bnj535  33383  bnj1463  33546
  Copyright terms: Public domain W3C validator