Theorem feq2 5256

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 5212	. . 3 |- ( A = B -> ( F Fn A <-> F Fn B ) )
2	1	anbi1d 460	. 2 |- ( A = B -> ( ( F Fn A /\ ran F C_ C ) <-> ( F Fn B /\ ran F C_ C ) ) )
3		df-f 5127	. 2 |- ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
4		df-f 5127	. 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 1331   C_ wss 3071   ran crn 4540   Fn wfn 5118   -->wf 5119

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-fn 5126  df-f 5127

This theorem is referenced by:  feq23  5258  feq2d  5260  feq2i  5266  f00  5314  f0dom0  5316  f1eq2  5324  fressnfv  5607  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  tfrcl  6261  mapvalg  6552  map0g  6582  ac6sfi  6792  isomni  7008  ismkv  7027