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 3960	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵))
2	1	anbi2d 630	. 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 1541   ⊆ wss 3901  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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918  df-f 6496

This theorem is referenced by:  feq23  6643  feq3d  6647  fun2  6697  fconstg  6721  f1eq3  6727  mapvalg  8773  mapsnd  8824  cantnff  9583  axdc4uz  13907  supcvg  15779  lmff  23245  txcn  23570  lmmbr  25214  iscmet3  25249  dvcnvrelem2  25979  itgsubstlem  26011  umgrislfupgr  29196  uspgriedgedg  29249  usgrislfuspgr  29260  wlkv0  29723  isgrpo  30572  vciOLD  30636  isvclem  30652  nmop0h  32066  sitgaddlemb  34505  sitmcl  34508  cvmliftlem15  35492  mtyf  35746  matunitlindflem1  37817  sdclem1  37944  k0004lem1  44388  relpeq5  45189  stoweidlem57  46301  f1ocof1ob  47327  isuspgrim0lem  48139  gricushgr  48163  uspgrlimlem4  48237  mof02  49084  mofsn2  49090  mofeu  49093  fdomne0  49095  f002  49099  fullthinc  49695  functermc  49753