Theorem feq2 5409

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 5363	. . 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 5275	. 2 |- ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
4		df-f 5275	. 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 1373   C_ wss 3166   ran crn 4676   Fn wfn 5266   -->wf 5267

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-fn 5274  df-f 5275

This theorem is referenced by:  feq23  5411  feq2d  5413  feq2i  5419  f00  5467  f0dom0  5469  f1eq2  5477  fressnfv  5771  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemaccex  6447  tfrcllemres  6448  tfrcldm  6449  tfrcl  6450  mapvalg  6745  map0g  6775  ac6sfi  6995  isomni  7238  ismkv  7255  iswomni  7267  isghm  13579