ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fneq2 Unicode version

Theorem fneq2 5324
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 2199 . . 3  |-  ( A  =  B  ->  ( dom  F  =  A  <->  dom  F  =  B ) )
21anbi2d 464 . 2  |-  ( A  =  B  ->  (
( Fun  F  /\  dom  F  =  A )  <-> 
( Fun  F  /\  dom  F  =  B ) ) )
3 df-fn 5238 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 df-fn 5238 . 2  |-  ( F  Fn  B  <->  ( Fun  F  /\  dom  F  =  B ) )
52, 3, 43bitr4g 223 1  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    = wceq 1364   dom cdm 4644   Fun wfun 5229    Fn wfn 5230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-fn 5238
This theorem is referenced by:  fneq2d  5326  fneq2i  5330  feq2  5368  foeq2  5454  f1o00  5515  eqfnfv2  5635  tfr0dm  6347  tfrlemisucaccv  6350  tfrlemi1  6357  tfrlemi14d  6358  tfrexlem  6359  tfr1onlemsucfn  6365  tfr1onlemsucaccv  6366  tfr1onlembxssdm  6368  tfr1onlembfn  6369  tfr1onlemaccex  6373  tfr1onlemres  6374  ixpeq1  6735  0fz1  10075
  Copyright terms: Public domain W3C validator