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

Theorem feq2 5697
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 5651 . . 3  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
21anbi1d 703 . 2  |-  ( A  =  B  ->  (
( F  Fn  A  /\  ran  F  C_  C
)  <->  ( F  Fn  B  /\  ran  F  C_  C ) ) )
3 df-f 5573 . 2  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
4 df-f 5573 . 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 367    = wceq 1405    C_ wss 3414   ran crn 4824    Fn wfn 5564   -->wf 5565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-cleq 2394  df-fn 5572  df-f 5573
This theorem is referenced by:  feq23  5699  feq2d  5701  feq2i  5707  f00  5750  f0dom0  5752  f1eq2  5760  fressnfv  6065  fconstfvOLD  6115  mapvalg  7467  map0g  7496  ac6sfi  7798  cofsmo  8681  axcc4dom  8853  ac6sg  8900  isghm  16591  pjdm2  19040  cmpcovf  20184  ulmval  23067  measval  28646  isrnmeas  28648  poseq  30064  soseq  30065  elno2  30114  noreson  30120  noxpsgn  30125  nodenselem6  30146  bj-finsumval0  31227  mbfresfi  31433  stoweidlem62  37212
  Copyright terms: Public domain W3C validator