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

Theorem feq3 5541
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 3375 . . 3  |-  ( A  =  B  ->  ( ran  F  C_  A  <->  ran  F  C_  B ) )
21anbi2d 698 . 2  |-  ( A  =  B  ->  (
( F  Fn  C  /\  ran  F  C_  A
)  <->  ( F  Fn  C  /\  ran  F  C_  B ) ) )
3 df-f 5419 . 2  |-  ( F : C --> A  <->  ( F  Fn  C  /\  ran  F  C_  A ) )
4 df-f 5419 . 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 1364    C_ wss 3325   ran crn 4837    Fn wfn 5410   -->wf 5411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-in 3332  df-ss 3339  df-f 5419
This theorem is referenced by:  feq23  5542  feq123d  5546  fun2  5573  fconstg  5594  f1eq3  5600  fsng  5879  fsn2  5880  fsnunf  5913  mapvalg  7220  mapsn  7250  cantnff  7878  axdc4uz  11801  supcvg  13314  funcres2b  14803  funcres2  14804  hofcl  15065  resmhm2b  15484  pwsdiagmhm  15492  gsumress  15500  frmdup3  15537  isghm  15740  frgpup3lem  16267  gsumzsubmcl  16395  gsumzsubmclOLD  16396  dmdprd  16470  frlmup2  18127  cnpf2  18754  lmff  18805  2ndcctbss  18959  1stcelcls  18965  uptx  19098  txcn  19099  tsmssubm  19616  cnextucn  19778  pi1addf  20519  lmmbr  20669  caufval  20686  iscmet3  20704  equivcau  20711  lmcau  20723  dvcnvrelem2  21390  itgsubstlem  21420  plypf1  21623  coef2  21642  ulmval  21788  isumgra  23168  wlks  23344  iseupa  23505  isgrpo  23602  elghomlem1  23767  vci  23845  isvclem  23874  vcoprnelem  23875  chscllem4  24962  nmop0h  25314  sibff  26636  sibfof  26640  cvmliftlem15  27101  ghomgrpilem2  27218  sdclem1  28548  isbnd3  28592  prdsbnd  28601  heibor  28629  stoweidlem57  29761  wlkelwrd  30189  wlkcompim  30196
  Copyright terms: Public domain W3C validator