Theorem feq3 6650

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3911  ran crn 5632   Fn wfn 6494  ⟶wf 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928  df-f 6503

This theorem is referenced by:  feq23  6651  feq3d  6655  fun2  6705  fconstg  6729  f1eq3  6735  mapvalg  8786  mapsnd  8836  cantnff  9603  axdc4uz  13925  supcvg  15798  lmff  23164  txcn  23489  lmmbr  25134  iscmet3  25169  dvcnvrelem2  25899  itgsubstlem  25931  umgrislfupgr  29026  uspgriedgedg  29079  usgrislfuspgr  29090  wlkv0  29553  isgrpo  30399  vciOLD  30463  isvclem  30479  nmop0h  31893  sitgaddlemb  34312  sitmcl  34315  cvmliftlem15  35258  mtyf  35512  matunitlindflem1  37583  sdclem1  37710  k0004lem1  44109  relpeq5  44911  stoweidlem57  46028  f1ocof1ob  47055  isuspgrim0lem  47866  gricushgr  47890  uspgrlimlem4  47963  mof02  48800  mofsn2  48806  mofeu  48809  fdomne0  48811  f002  48815  fullthinc  49412  functermc  49470