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

Theorem feq3 5544
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 3378 . . 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 5422 . 2  |-  ( F : C --> A  <->  ( F  Fn  C  /\  ran  F  C_  A ) )
4 df-f 5422 . 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 1369    C_ wss 3328   ran crn 4841    Fn wfn 5413   -->wf 5414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3335  df-ss 3342  df-f 5422
This theorem is referenced by:  feq23  5545  feq123d  5549  fun2  5576  fconstg  5597  f1eq3  5603  fsng  5882  fsn2  5883  fsnunf  5916  mapvalg  7224  mapsn  7254  cantnff  7882  axdc4uz  11805  supcvg  13318  funcres2b  14807  funcres2  14808  hofcl  15069  resmhm2b  15489  pwsdiagmhm  15497  gsumress  15507  frmdup3  15544  isghm  15747  frgpup3lem  16274  gsumzsubmcl  16402  gsumzsubmclOLD  16403  dmdprd  16480  frlmup2  18227  cnpf2  18854  lmff  18905  2ndcctbss  19059  1stcelcls  19065  uptx  19198  txcn  19199  tsmssubm  19716  cnextucn  19878  pi1addf  20619  lmmbr  20769  caufval  20786  iscmet3  20804  equivcau  20811  lmcau  20823  dvcnvrelem2  21490  itgsubstlem  21520  plypf1  21680  coef2  21699  ulmval  21845  isumgra  23249  wlks  23425  iseupa  23586  isgrpo  23683  elghomlem1  23848  vci  23926  isvclem  23955  vcoprnelem  23956  chscllem4  25043  nmop0h  25395  sibff  26722  sibfof  26726  cvmliftlem15  27187  ghomgrpilem2  27305  sdclem1  28639  isbnd3  28683  prdsbnd  28692  heibor  28720  stoweidlem57  29852  wlkelwrd  30280  wlkcompim  30287
  Copyright terms: Public domain W3C validator