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

Theorem feq2 5538
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 5495 . . 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 5417 . 2  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
4 df-f 5417 . 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 1369    C_ wss 3323   ran crn 4836    Fn wfn 5408   -->wf 5409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-fn 5416  df-f 5417
This theorem is referenced by:  feq23  5540  feq2d  5542  feq2i  5547  f00  5588  f0dom0  5590  f1eq2  5597  fressnfv  5891  fconstfv  5935  mapvalg  7216  map0g  7244  ac6sfi  7548  cofsmo  8430  axcc4dom  8602  ac6sg  8649  isghm  15738  pjdm2  18111  cmpcovf  18969  ulmval  21820  measval  26564  isrnmeas  26566  poseq  27665  soseq  27666  elno2  27746  noreson  27752  noxpsgn  27757  nodenselem6  27778  mbfresfi  28391  stoweidlem62  29810  bj-finsumval0  32426
  Copyright terms: Public domain W3C validator