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

Theorem fneq2 5611
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 2469 . . 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 5532 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 df-fn 5532 . 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 1370   dom cdm 4951   Fun wfun 5523    Fn wfn 5524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2446  df-fn 5532
This theorem is referenced by:  fneq2d  5613  fneq2i  5617  feq2  5654  foeq2  5728  f1o00  5784  eqfnfv2  5910  fconstfv  6052  tfrlem12  6961  ixpeq1  7387  ac5  8760  0fz1  11589  wfrlem1  27888  wfrlem15  27902  frrlem1  27932  fnchoice  29919  bnj90  32063  bnj919  32112  bnj535  32235  bnj1463  32398
  Copyright terms: Public domain W3C validator