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

Theorem feq2 5712
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 5668 . . 3  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
21anbi1d 704 . 2  |-  ( A  =  B  ->  (
( F  Fn  A  /\  ran  F  C_  C
)  <->  ( F  Fn  B  /\  ran  F  C_  C ) ) )
3 df-f 5590 . 2  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
4 df-f 5590 . 2  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
52, 3, 43bitr4g 288 1  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    C_ wss 3476   ran crn 5000    Fn wfn 5581   -->wf 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fn 5589  df-f 5590
This theorem is referenced by:  feq23  5714  feq2d  5716  feq2i  5722  f00  5765  f0dom0  5767  f1eq2  5775  fressnfv  6073  fconstfv  6121  mapvalg  7427  map0g  7455  ac6sfi  7760  cofsmo  8645  axcc4dom  8817  ac6sg  8864  isghm  16062  pjdm2  18509  cmpcovf  19657  ulmval  22509  measval  27809  isrnmeas  27811  poseq  28910  soseq  28911  elno2  28991  noreson  28997  noxpsgn  29002  nodenselem6  29023  mbfresfi  29638  stoweidlem62  31362  fourierdlem60  31467  fourierdlem61  31468  fourierdlem81  31488  bj-finsumval0  33735
  Copyright terms: Public domain W3C validator