Theorem feq3 6642

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 3949	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵))
2	1	anbi2d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵)))
3		df-f 6496	. 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴))
4		df-f 6496	. 2 ⊢ (𝐹:𝐶⟶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ⊆ wss 3890  ran crn 5625   Fn wfn 6487  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907  df-f 6496

This theorem is referenced by:  feq23  6643  feq3d  6647  fun2  6697  fconstg  6721  f1eq3  6727  mapvalg  8776  mapsnd  8827  cantnff  9586  axdc4uz  13937  supcvg  15812  lmff  23276  txcn  23601  lmmbr  25235  iscmet3  25270  dvcnvrelem2  25995  itgsubstlem  26025  umgrislfupgr  29206  uspgriedgedg  29259  usgrislfuspgr  29270  wlkv0  29733  isgrpo  30583  vciOLD  30647  isvclem  30663  nmop0h  32077  sitgaddlemb  34508  sitmcl  34511  cvmliftlem15  35496  mtyf  35750  matunitlindflem1  37951  sdclem1  38078  k0004lem1  44592  relpeq5  45393  stoweidlem57  46503  f1ocof1ob  47541  isuspgrim0lem  48381  gricushgr  48405  uspgrlimlem4  48479  mof02  49326  mofsn2  49332  mofeu  49335  fdomne0  49337  f002  49341  fullthinc  49937  functermc  49995