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

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

Proof of Theorem feq3
StepHypRef Expression
1 sseq2 3330 . . 3  |-  ( A  =  B  ->  ( ran  F  C_  A  <->  ran  F  C_  B ) )
21anbi2d 685 . 2  |-  ( A  =  B  ->  (
( F  Fn  C  /\  ran  F  C_  A
)  <->  ( F  Fn  C  /\  ran  F  C_  B ) ) )
3 df-f 5417 . 2  |-  ( F : C --> A  <->  ( F  Fn  C  /\  ran  F  C_  A ) )
4 df-f 5417 . 2  |-  ( F : C --> B  <->  ( F  Fn  C  /\  ran  F  C_  B ) )
52, 3, 43bitr4g 280 1  |-  ( A  =  B  ->  ( F : C --> A  <->  F : C
--> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    C_ wss 3280   ran crn 4838    Fn wfn 5408   -->wf 5409
This theorem is referenced by:  feq23  5538  feq123d  5542  fun2  5567  fconstg  5589  f1eq3  5595  fsng  5866  fsn2  5867  fsnunf  5890  mapvalg  6987  mapsn  7014  cantnff  7585  axdc4uz  11277  supcvg  12590  funcres2b  14049  funcres2  14050  hofcl  14311  resmhm2b  14716  pwsdiagmhm  14723  gsumress  14732  frmdup3  14766  isghm  14961  frgpup3lem  15364  gsumzsubmcl  15478  dmdprd  15514  cnpf2  17268  lmff  17319  2ndcctbss  17471  1stcelcls  17477  uptx  17610  txcn  17611  tsmssubm  18125  cnextucn  18286  pi1addf  19025  lmmbr  19164  caufval  19181  iscmet3  19199  equivcau  19206  lmcau  19218  dvcnvrelem2  19855  itgsubstlem  19885  plypf1  20084  coef2  20103  ulmval  20249  isumgra  21303  wlks  21479  iseupa  21640  isgrpo  21737  elghomlem1  21902  vci  21980  isvclem  22009  vcoprnelem  22010  chscllem4  23095  nmop0h  23447  sibff  24604  sibfof  24607  sitmcl  24616  cvmliftlem15  24938  ghomgrpilem2  25050  sdclem1  26337  isbnd3  26383  prdsbnd  26392  heibor  26420  frlmup2  27119  stoweidlem57  27673
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294  df-f 5417
  Copyright terms: Public domain W3C validator