Theorem feq3 6718

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ⊆ wss 3962  ran crn 5689   Fn wfn 6557  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979  df-f 6566

This theorem is referenced by:  feq23  6719  feq3d  6723  fun2  6771  fconstg  6795  f1eq3  6801  mapvalg  8874  mapsnd  8924  cantnff  9711  axdc4uz  14021  supcvg  15888  lmff  23324  txcn  23649  lmmbr  25305  iscmet3  25340  dvcnvrelem2  26071  itgsubstlem  26103  umgrislfupgr  29154  uspgriedgedg  29207  usgrislfuspgr  29218  wlkv0  29683  isgrpo  30525  vciOLD  30589  isvclem  30605  nmop0h  32019  sitgaddlemb  34329  sitmcl  34332  cvmliftlem15  35282  mtyf  35536  matunitlindflem1  37602  sdclem1  37729  k0004lem1  44136  stoweidlem57  46012  f1ocof1ob  47030  isuspgrim0lem  47808  gricushgr  47823  uspgrlimlem4  47893  mof02  48668  mofsn2  48674  mofeu  48677  fdomne0  48679  f002  48683  fullthinc  48845