Theorem feq3 6675

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ⊆ wss 3907  ran crn 5652   Fn wfn 6520  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924  df-f 6529

This theorem is referenced by:  feq23  6676  feq3d  6680  fun2  6731  fconstg  6755  f1eq3  6761  mapvalg  8821  mapsnd  8872  cantnff  9631  axdc4uz  14008  supcvg  15898  lmff  23415  txcn  23740  lmmbr  25374  iscmet3  25409  dvcnvrelem2  26134  itgsubstlem  26164  umgrislfupgr  29378  uspgriedgedg  29431  usgrislfuspgr  29442  wlkv0  29904  isgrpo  30754  vciOLD  30818  isvclem  30834  nmop0h  32248  sitgaddlemb  34650  sitmcl  34653  cvmliftlem15  35656  mtyf  35910  matunitlindflem1  38122  sdclem1  38249  k0004lem1  44730  relpeq5  45516  stoweidlem57  46630  f1ocof1ob  47674  isuspgrim0lem  48514  gricushgr  48538  uspgrlimlem4  48612  mof02  49469  mofsn2  49475  mofeu  49478  fdomne0  49480  f002  49484  fullthinc  50080  functermc  50138