Theorem feq3 5474

Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
feq3	|- ( A = B -> ( F : C --> A <-> F : C --> B ) )

Proof of Theorem feq3

Step	Hyp	Ref	Expression
1		sseq2 3252	. . 3 |- ( A = B -> ( ran F C_ A <-> ran F C_ B ) )
2	1	anbi2d 464	. 2 |- ( A = B -> ( ( F Fn C /\ ran F C_ A ) <-> ( F Fn C /\ ran F C_ B ) ) )
3		df-f 5337	. 2 |- ( F : C --> A <-> ( F Fn C /\ ran F C_ A ) )
4		df-f 5337	. 2 |- ( F : C --> B <-> ( F Fn C /\ ran F C_ B ) )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( F : C --> A <-> F : C --> B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1398   C_ wss 3201   ran crn 4732   Fn wfn 5328   -->wf 5329

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214  df-f 5337

This theorem is referenced by:  feq23  5475  feq3d  5478  feq123d  5480  fun2  5517  fconstg  5542  f1eq3  5548  fsng  5828  fsn2  5829  fsnunf  5862  mapvalg  6870  mapsn  6902  lmff  15060  txcn  15086  plyrecj  15574  umgrislfupgrdom  16072  uspgriedgedg  16120  usgrislfuspgrdom  16131  subupgr  16214  wlkv0  16310