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

Theorem feq2 5606
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
feq2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 5564 . . 3  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
21anbi1d 687 . 2  |-  ( A  =  B  ->  (
( F  Fn  A  /\  ran  F  C_  C
)  <->  ( F  Fn  B  /\  ran  F  C_  C ) ) )
3 df-f 5487 . 2  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
4 df-f 5487 . 2  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
52, 3, 43bitr4g 281 1  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    C_ wss 3306   ran crn 4908    Fn wfn 5478   -->wf 5479
This theorem is referenced by:  feq23  5608  feq2d  5610  feq2i  5615  f00  5657  f1eq2  5664  fressnfv  5949  fconstfv  5983  mapvalg  7057  map0g  7082  ac6sfi  7380  cofsmo  8180  axcc4dom  8352  ac6sg  8399  isghm  15037  pjdm2  16969  cmpcovf  17485  ulmval  20327  measval  24583  isrnmeas  24585  poseq  25559  soseq  25560  elno2  25640  noreson  25646  noxpsgn  25651  nodenselem6  25672  mbfresfi  26289  stoweidlem62  27825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-11 1763  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2435  df-fn 5486  df-f 5487
  Copyright terms: Public domain W3C validator