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

Theorem fneq2 5039
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 2092 . . 3  |-  ( A  =  B  ->  ( dom  F  =  A  <->  dom  F  =  B ) )
21anbi2d 452 . 2  |-  ( A  =  B  ->  (
( Fun  F  /\  dom  F  =  A )  <-> 
( Fun  F  /\  dom  F  =  B ) ) )
3 df-fn 4955 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 df-fn 4955 . 2  |-  ( F  Fn  B  <->  ( Fun  F  /\  dom  F  =  B ) )
52, 3, 43bitr4g 221 1  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1285   dom cdm 4391   Fun wfun 4946    Fn wfn 4947
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-fn 4955
This theorem is referenced by:  fneq2d  5041  fneq2i  5045  feq2  5082  foeq2  5154  f1o00  5212  eqfnfv2  5318  tfr0dm  5991  tfrlemisucaccv  5994  tfrlemi1  6001  tfrlemi14d  6002  tfrexlem  6003  tfr1onlemsucfn  6009  tfr1onlemsucaccv  6010  tfr1onlembxssdm  6012  tfr1onlembfn  6013  tfr1onlemaccex  6017  tfr1onlemres  6018  0fz1  9192
  Copyright terms: Public domain W3C validator