Theorem feq3 6470

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ⊆ wss 3881  ran crn 5520   Fn wfn 6319  ⟶wf 6320

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-f 6328

This theorem is referenced by:  feq23  6471  feq3d  6474  fun2  6515  fconstg  6540  f1eq3  6546  mapvalg  8399  mapsnd  8433  cantnff  9121  axdc4uz  13347  supcvg  15203  lmff  21906  txcn  22231  lmmbr  23862  iscmet3  23897  dvcnvrelem2  24621  itgsubstlem  24651  umgrislfupgr  26916  usgrislfuspgr  26977  wlkv0  27440  isgrpo  28280  vciOLD  28344  isvclem  28360  nmop0h  29774  sitgaddlemb  31716  sitmcl  31719  cvmliftlem15  32658  mtyf  32912  matunitlindflem1  35053  sdclem1  35181  k0004lem1  40850  stoweidlem57  42699  isomushgr  44344