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

Theorem feq3 5570
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 3362 . . 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 5450 . 2  |-  ( F : C --> A  <->  ( F  Fn  C  /\  ran  F  C_  A ) )
4 df-f 5450 . 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 1652    C_ wss 3312   ran crn 4871    Fn wfn 5441   -->wf 5442
This theorem is referenced by:  feq23  5571  feq123d  5575  fun2  5600  fconstg  5622  f1eq3  5628  fsng  5899  fsn2  5900  fsnunf  5923  mapvalg  7020  mapsn  7047  cantnff  7621  axdc4uz  11314  supcvg  12627  funcres2b  14086  funcres2  14087  hofcl  14348  resmhm2b  14753  pwsdiagmhm  14760  gsumress  14769  frmdup3  14803  isghm  14998  frgpup3lem  15401  gsumzsubmcl  15515  dmdprd  15551  cnpf2  17306  lmff  17357  2ndcctbss  17510  1stcelcls  17516  uptx  17649  txcn  17650  tsmssubm  18164  cnextucn  18325  pi1addf  19064  lmmbr  19203  caufval  19220  iscmet3  19238  equivcau  19245  lmcau  19257  dvcnvrelem2  19894  itgsubstlem  19924  plypf1  20123  coef2  20142  ulmval  20288  isumgra  21342  wlks  21518  iseupa  21679  isgrpo  21776  elghomlem1  21941  vci  22019  isvclem  22048  vcoprnelem  22049  chscllem4  23134  nmop0h  23486  sibff  24643  sibfof  24646  sitmcl  24655  cvmliftlem15  24977  ghomgrpilem2  25089  sdclem1  26438  isbnd3  26484  prdsbnd  26493  heibor  26521  frlmup2  27219  stoweidlem57  27773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326  df-f 5450
  Copyright terms: Public domain W3C validator