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

Theorem feq3 5705
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 3511 . . 3  |-  ( A  =  B  ->  ( ran  F  C_  A  <->  ran  F  C_  B ) )
21anbi2d 703 . 2  |-  ( A  =  B  ->  (
( F  Fn  C  /\  ran  F  C_  A
)  <->  ( F  Fn  C  /\  ran  F  C_  B ) ) )
3 df-f 5582 . 2  |-  ( F : C --> A  <->  ( F  Fn  C  /\  ran  F  C_  A ) )
4 df-f 5582 . 2  |-  ( F : C --> B  <->  ( F  Fn  C  /\  ran  F  C_  B ) )
52, 3, 43bitr4g 288 1  |-  ( A  =  B  ->  ( F : C --> A  <->  F : C
--> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383    C_ wss 3461   ran crn 4990    Fn wfn 5573   -->wf 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475  df-f 5582
This theorem is referenced by:  feq23  5706  feq3d  5709  fun2  5739  fconstg  5762  f1eq3  5768  mapvalg  7432  mapsn  7462  cantnff  8096  axdc4uz  12075  supcvg  13649  gsumzsubmclOLD  16908  lmff  19780  txcn  20105  lmmbr  21675  iscmet3  21710  dvcnvrelem2  22397  itgsubstlem  22427  isumgra  24293  wlks  24497  wlkcompim  24504  wlkelwrd  24508  iseupa  24943  isgrpo  25176  vci  25419  isvclem  25448  vcoprnelem  25449  nmop0h  26888  cvmliftlem15  28721  mtyf  28890  ghomgrpilem2  29004  sdclem1  30212  stoweidlem57  31793  uhgrepe  32332
  Copyright terms: Public domain W3C validator