Theorem feq3 6583

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

Assertion

Ref	Expression
feq3	⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵))

Proof of Theorem feq3

Step	Hyp	Ref	Expression
1		sseq2 3947	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵))
2	1	anbi2d 629	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵)))
3		df-f 6437	. 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴))
4		df-f 6437	. 2 ⊢ (𝐹:𝐶⟶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ⊆ wss 3887  ran crn 5590   Fn wfn 6428  ⟶wf 6429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-f 6437

This theorem is referenced by:  feq23  6584  feq3d  6587  fun2  6637  fconstg  6661  f1eq3  6667  mapvalg  8625  mapsnd  8674  cantnff  9432  axdc4uz  13704  supcvg  15568  lmff  22452  txcn  22777  lmmbr  24422  iscmet3  24457  dvcnvrelem2  25182  itgsubstlem  25212  umgrislfupgr  27493  usgrislfuspgr  27554  wlkv0  28018  isgrpo  28859  vciOLD  28923  isvclem  28939  nmop0h  30353  sitgaddlemb  32315  sitmcl  32318  cvmliftlem15  33260  mtyf  33514  matunitlindflem1  35773  sdclem1  35901  k0004lem1  41757  stoweidlem57  43598  f1ocof1ob  44573  isomushgr  45278  mof02  46166  mofsn2  46172  mofeu  46175  fdomne0  46177  f002  46181  fullthinc  46327