Theorem feq3 6639

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ⊆ wss 3898  ran crn 5622   Fn wfn 6484  ⟶wf 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915  df-f 6493

This theorem is referenced by:  feq23  6640  feq3d  6644  fun2  6694  fconstg  6718  f1eq3  6724  mapvalg  8769  mapsnd  8820  cantnff  9575  axdc4uz  13898  supcvg  15770  lmff  23236  txcn  23561  lmmbr  25205  iscmet3  25240  dvcnvrelem2  25970  itgsubstlem  26002  umgrislfupgr  29122  uspgriedgedg  29175  usgrislfuspgr  29186  wlkv0  29649  isgrpo  30498  vciOLD  30562  isvclem  30578  nmop0h  31992  sitgaddlemb  34433  sitmcl  34436  cvmliftlem15  35414  mtyf  35668  matunitlindflem1  37729  sdclem1  37856  k0004lem1  44304  relpeq5  45105  stoweidlem57  46217  f1ocof1ob  47243  isuspgrim0lem  48055  gricushgr  48079  uspgrlimlem4  48153  mof02  49000  mofsn2  49006  mofeu  49009  fdomne0  49011  f002  49015  fullthinc  49611  functermc  49669