Theorem feq3 6239

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 385   = wceq 1653   ⊆ wss 3769  ran crn 5313   Fn wfn 6096  ⟶wf 6097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-in 3776  df-ss 3783  df-f 6105

This theorem is referenced by:  feq23  6240  feq3d  6243  fun2  6282  fconstg  6307  f1eq3  6313  mapvalg  8105  mapsnd  8137  cantnff  8821  axdc4uz  13038  supcvg  14926  lmff  21434  txcn  21758  lmmbr  23384  iscmet3  23419  dvcnvrelem2  24122  itgsubstlem  24152  umgrislfupgr  26358  usgrislfuspgr  26420  wlkv0  26900  isgrpo  27877  vciOLD  27941  isvclem  27957  nmop0h  29375  sitgaddlemb  30926  sitmcl  30929  cvmliftlem15  31797  mtyf  31966  matunitlindflem1  33894  sdclem1  34026  k0004lem1  39227  stoweidlem57  41017  isomushgr  42496