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

Theorem fneq2 5350
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 2305 . . 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 5274 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 df-fn 5274 . 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 1632   dom cdm 4705   Fun wfun 5265    Fn wfn 5266
This theorem is referenced by:  fneq2d  5352  fneq2i  5355  feq2  5392  foeq2  5464  f1o00  5524  eqfnfv2  5639  fconstfv  5750  tfrlem3  6409  tfrlem12  6421  ixpeq1  6843  ac5  8120  0fz1  10829  wfrlem1  24327  wfrlem15  24341  frrlem1  24352  bpolyval  24856  ac5g  25178  fnchoice  27803  bnj90  29064  bnj919  29113  bnj535  29238  bnj1463  29401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289  df-fn 5274
  Copyright terms: Public domain W3C validator