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

Theorem feq3 5518
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 3313 . . 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 5398 . 2  |-  ( F : C --> A  <->  ( F  Fn  C  /\  ran  F  C_  A ) )
4 df-f 5398 . 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 3263   ran crn 4819    Fn wfn 5389   -->wf 5390
This theorem is referenced by:  feq23  5519  feq123d  5523  fun2  5548  fconstg  5570  f1eq3  5576  fsng  5846  fsn2  5847  fsnunf  5870  mapvalg  6964  mapsn  6991  cantnff  7562  axdc4uz  11249  supcvg  12562  funcres2b  14021  funcres2  14022  hofcl  14283  resmhm2b  14688  pwsdiagmhm  14695  gsumress  14704  frmdup3  14738  isghm  14933  frgpup3lem  15336  gsumzsubmcl  15450  dmdprd  15486  cnpf2  17236  lmff  17287  2ndcctbss  17439  1stcelcls  17445  uptx  17578  txcn  17579  tsmssubm  18093  cnextucn  18254  pi1addf  18943  lmmbr  19082  caufval  19099  iscmet3  19117  equivcau  19124  lmcau  19136  dvcnvrelem2  19769  itgsubstlem  19799  plypf1  19998  coef2  20017  ulmval  20163  isumgra  21217  wlks  21390  iseupa  21535  isgrpo  21632  elghomlem1  21797  vci  21875  isvclem  21904  vcoprnelem  21905  chscllem4  22990  nmop0h  23342  cvmliftlem15  24764  ghomgrpilem2  24876  sdclem1  26138  isbnd3  26184  prdsbnd  26193  heibor  26221  frlmup2  26920  stoweidlem57  27474
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
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 2374  df-cleq 2380  df-clel 2383  df-in 3270  df-ss 3277  df-f 5398
  Copyright terms: Public domain W3C validator