Theorem feq2 5350

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 5306	. . 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 5221	. 2 |- ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
4		df-f 5221	. 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 1353   C_ wss 3130   ran crn 4628   Fn wfn 5212   -->wf 5213

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-fn 5220  df-f 5221

This theorem is referenced by:  feq23  5352  feq2d  5354  feq2i  5360  f00  5408  f0dom0  5410  f1eq2  5418  fressnfv  5704  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemaccex  6362  tfrcllemres  6363  tfrcldm  6364  tfrcl  6365  mapvalg  6658  map0g  6688  ac6sfi  6898  isomni  7134  ismkv  7151  iswomni  7163