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

Theorem feq3 5393
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 3213 . . 3  |-  ( A  =  B  ->  ( ran  F  C_  A  <->  ran  F  C_  B ) )
21anbi2d 684 . 2  |-  ( A  =  B  ->  (
( F  Fn  C  /\  ran  F  C_  A
)  <->  ( F  Fn  C  /\  ran  F  C_  B ) ) )
3 df-f 5275 . 2  |-  ( F : C --> A  <->  ( F  Fn  C  /\  ran  F  C_  A ) )
4 df-f 5275 . 2  |-  ( F : C --> B  <->  ( F  Fn  C  /\  ran  F  C_  B ) )
52, 3, 43bitr4g 279 1  |-  ( A  =  B  ->  ( F : C --> A  <->  F : C
--> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    C_ wss 3165   ran crn 4706    Fn wfn 5266   -->wf 5267
This theorem is referenced by:  feq23  5394  feq123d  5398  fun2  5422  fconstg  5444  f1eq3  5450  fsng  5713  fsn2  5714  fsnunf  5734  mapvalg  6798  mapsn  6825  cantnff  7391  axdc4uz  11061  supcvg  12330  funcres2b  13787  funcres2  13788  hofcl  14049  resmhm2b  14454  pwsdiagmhm  14461  gsumress  14470  frmdup3  14504  isghm  14699  frgpup3lem  15102  gsumzsubmcl  15216  dmdprd  15252  cnpf2  16996  lmff  17045  2ndcctbss  17197  1stcelcls  17203  uptx  17335  txcn  17336  tsmssubm  17841  pi1addf  18561  lmmbr  18700  caufval  18717  iscmet3  18735  equivcau  18742  lmcau  18754  dvcnvrelem2  19381  itgsubstlem  19411  plypf1  19610  coef2  19629  ulmval  19775  isgrpo  20879  elghomlem1  21044  vci  21120  isvclem  21149  vcoprnelem  21150  chscllem4  22235  nmop0h  22587  cvmliftlem15  23844  isumgra  23882  iseupa  23896  ghomgrpilem2  24008  limptlimpr2lem1  25677  limptlimpr2lem2  25678  flfneic  25727  ismgra  25813  isalg  25824  algi  25830  aidm2  25853  dualalg  25885  sdclem1  26556  isbnd3  26611  prdsbnd  26620  heibor  26648  frlmup2  27354  stoweidlem57  27909  wlks  28328
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-f 5275
  Copyright terms: Public domain W3C validator