Theorem feq2 5512

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 5465	. . 3 |- ( A = B -> ( F Fn A <-> F Fn B ) )
2	1	anbi1d 469	. 2 |- ( A = B -> ( ( F Fn A /\ ran F C_ C ) <-> ( F Fn B /\ ran F C_ C ) ) )
3		df-f 5376	. 2 |- ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
4		df-f 5376	. 2 |- ( F : B --> C <-> ( F Fn B /\ ran F C_ C ) )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( F : A --> C <-> F : B --> C ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   C_ wss 3220   ran crn 4770   Fn wfn 5367   -->wf 5368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5375  df-f 5376

This theorem is referenced by:  feq23  5514  feq2d  5516  feq2i  5522  f00  5579  f0dom0  5581  f1eq2  5589  fressnfv  5893  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemaccex  6622  tfrcllemres  6623  tfrcldm  6624  tfrcl  6625  mapvalg  6922  map0g  6959  ac6sfi  7192  isomni  7466  ismkv  7483  iswomni  7495  isghm  14023