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

Theorem feq3 5715
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 3526 . . 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 5592 . 2  |-  ( F : C --> A  <->  ( F  Fn  C  /\  ran  F  C_  A ) )
4 df-f 5592 . 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 1379    C_ wss 3476   ran crn 5000    Fn wfn 5583   -->wf 5584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-f 5592
This theorem is referenced by:  feq23  5716  feq3d  5719  feq123d  5721  fun2  5749  fconstg  5772  f1eq3  5778  fsng  6060  fsn2  6061  fsnunf  6099  mapvalg  7430  mapsn  7460  cantnff  8093  axdc4uz  12061  supcvg  13630  funcres2b  15124  funcres2  15125  hofcl  15386  resmhm2b  15811  pwsdiagmhm  15819  gsumress  15829  frmdup3  15866  isghm  16072  frgpup3lem  16601  gsumzsubmcl  16731  gsumzsubmclOLD  16732  dmdprd  16832  frlmup2  18628  scmatghm  18830  cnpf2  19545  lmff  19596  2ndcctbss  19750  1stcelcls  19756  uptx  19889  txcn  19890  tsmssubm  20407  cnextucn  20569  pi1addf  21310  lmmbr  21460  caufval  21477  iscmet3  21495  equivcau  21502  lmcau  21514  dvcnvrelem2  22182  itgsubstlem  22212  plypf1  22372  coef2  22391  ulmval  22537  isumgra  24019  wlks  24223  wlkcompim  24230  wlkelwrd  24234  iseupa  24669  isgrpo  24902  elghomlem1  25067  vci  25145  isvclem  25174  vcoprnelem  25175  chscllem4  26262  nmop0h  26614  sibff  27946  sibfof  27950  cvmliftlem15  28411  ghomgrpilem2  28529  sdclem1  29867  isbnd3  29911  prdsbnd  29920  heibor  29948  stoweidlem57  31385  uhgrepe  31873
  Copyright terms: Public domain W3C validator