Theorem feq3 6635

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ⊆ wss 3883  ran crn 5619   Fn wfn 6480  ⟶wf 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900  df-f 6489

This theorem is referenced by:  feq23  6636  feq3d  6640  fun2  6690  fconstg  6714  f1eq3  6720  mapvalg  8773  mapsnd  8824  cantnff  9586  axdc4uz  13937  supcvg  15812  lmff  23284  txcn  23609  lmmbr  25243  iscmet3  25278  dvcnvrelem2  26003  itgsubstlem  26033  umgrislfupgr  29210  uspgriedgedg  29263  usgrislfuspgr  29274  wlkv0  29736  isgrpo  30586  vciOLD  30650  isvclem  30666  nmop0h  32080  sitgaddlemb  34532  sitmcl  34535  cvmliftlem15  35526  mtyf  35780  matunitlindflem1  37983  sdclem1  38110  k0004lem1  44591  relpeq5  45392  stoweidlem57  46500  f1ocof1ob  47544  isuspgrim0lem  48384  gricushgr  48408  uspgrlimlem4  48482  mof02  49329  mofsn2  49335  mofeu  49338  fdomne0  49340  f002  49344  fullthinc  49940  functermc  49998