Theorem feq2 5302

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

Step	Hyp	Ref	Expression
1		fneq2 5258	. . 3 |- ( A = B -> ( F Fn A <-> F Fn B ) )
2	1	anbi1d 461	. 2 |- ( A = B -> ( ( F Fn A /\ ran F C_ C ) <-> ( F Fn B /\ ran F C_ C ) ) )
3		df-f 5173	. 2 |- ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
4		df-f 5173	. 2 |- ( F : B --> C <-> ( F Fn B /\ ran F C_ C ) )
5	2, 3, 4	3bitr4g 222	1 |- ( A = B -> ( F : A --> C <-> F : B --> C ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1335   C_ wss 3102   ran crn 4586   Fn wfn 5164   -->wf 5165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-fn 5172  df-f 5173

This theorem is referenced by:  feq23  5304  feq2d  5306  feq2i  5312  f00  5360  f0dom0  5362  f1eq2  5370  fressnfv  5653  tfrcllemsucfn  6297  tfrcllemsucaccv  6298  tfrcllembxssdm  6300  tfrcllembfn  6301  tfrcllemaccex  6305  tfrcllemres  6306  tfrcldm  6307  tfrcl  6308  mapvalg  6600  map0g  6630  ac6sfi  6840  isomni  7073  ismkv  7090  iswomni  7102