Theorem feq2 5517

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 5470	. . 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 5381	. 2 |- ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
4		df-f 5381	. 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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   C_ wss 3220   ran crn 4775   Fn wfn 5372   -->wf 5373

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5380  df-f 5381

This theorem is used by:  feq23  5519  feq2d  5521  feq2i  5527  f00  5584  f0dom0  5586  f1eq2  5594  fressnfv  5902  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  tfrcl  6635  mapvalg  6932  map0g  6969  ac6sfi  7202  isomni  7476  ismkv  7493  iswomni  7505  isghm  14046