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

Theorem feq2 5650
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
feq2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 5607 . . 3  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
21anbi1d 704 . 2  |-  ( A  =  B  ->  (
( F  Fn  A  /\  ran  F  C_  C
)  <->  ( F  Fn  B  /\  ran  F  C_  C ) ) )
3 df-f 5529 . 2  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
4 df-f 5529 . 2  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
52, 3, 43bitr4g 288 1  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370    C_ wss 3435   ran crn 4948    Fn wfn 5520   -->wf 5521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2446  df-fn 5528  df-f 5529
This theorem is referenced by:  feq23  5652  feq2d  5654  feq2i  5659  f00  5700  f0dom0  5702  f1eq2  5709  fressnfv  6004  fconstfv  6048  mapvalg  7333  map0g  7361  ac6sfi  7666  cofsmo  8548  axcc4dom  8720  ac6sg  8767  isghm  15865  pjdm2  18260  cmpcovf  19125  ulmval  21977  measval  26756  isrnmeas  26758  poseq  27857  soseq  27858  elno2  27938  noreson  27944  noxpsgn  27949  nodenselem6  27970  mbfresfi  28585  stoweidlem62  30004  bj-finsumval0  32906
  Copyright terms: Public domain W3C validator