Theorem feq3 6636

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3905  ran crn 5624   Fn wfn 6481  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922  df-f 6490

This theorem is referenced by:  feq23  6637  feq3d  6641  fun2  6691  fconstg  6715  f1eq3  6721  mapvalg  8770  mapsnd  8820  cantnff  9589  axdc4uz  13910  supcvg  15782  lmff  23205  txcn  23530  lmmbr  25175  iscmet3  25210  dvcnvrelem2  25940  itgsubstlem  25972  umgrislfupgr  29087  uspgriedgedg  29140  usgrislfuspgr  29151  wlkv0  29614  isgrpo  30460  vciOLD  30524  isvclem  30540  nmop0h  31954  sitgaddlemb  34335  sitmcl  34338  cvmliftlem15  35290  mtyf  35544  matunitlindflem1  37615  sdclem1  37742  k0004lem1  44140  relpeq5  44942  stoweidlem57  46058  f1ocof1ob  47085  isuspgrim0lem  47897  gricushgr  47921  uspgrlimlem4  47995  mof02  48843  mofsn2  48849  mofeu  48852  fdomne0  48854  f002  48858  fullthinc  49455  functermc  49513