Theorem feq2 5466

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 5419	. . 3 |- ( A = B -> ( F Fn A <-> F Fn B ) )
2	1	anbi1d 465	. 2 |- ( A = B -> ( ( F Fn A /\ ran F C_ C ) <-> ( F Fn B /\ ran F C_ C ) ) )
3		df-f 5330	. 2 |- ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
4		df-f 5330	. 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 1397   C_ wss 3200   ran crn 4726   Fn wfn 5321   -->wf 5322

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-fn 5329  df-f 5330

This theorem is referenced by:  feq23  5468  feq2d  5470  feq2i  5476  f00  5528  f0dom0  5530  f1eq2  5538  fressnfv  5840  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemaccex  6526  tfrcllemres  6527  tfrcldm  6528  tfrcl  6529  mapvalg  6826  map0g  6856  ac6sfi  7086  isomni  7334  ismkv  7351  iswomni  7363  isghm  13829