Theorem feq3 6697

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ⊆ wss 3947  ran crn 5676   Fn wfn 6535  ⟶wf 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-f 6544

This theorem is referenced by:  feq23  6698  feq3d  6701  fun2  6751  fconstg  6775  f1eq3  6781  mapvalg  8826  mapsnd  8876  cantnff  9665  axdc4uz  13945  supcvg  15798  lmff  22796  txcn  23121  lmmbr  24766  iscmet3  24801  dvcnvrelem2  25526  itgsubstlem  25556  umgrislfupgr  28372  usgrislfuspgr  28433  wlkv0  28897  isgrpo  29737  vciOLD  29801  isvclem  29817  nmop0h  31231  sitgaddlemb  33335  sitmcl  33338  cvmliftlem15  34277  mtyf  34531  matunitlindflem1  36472  sdclem1  36599  k0004lem1  42883  stoweidlem57  44759  f1ocof1ob  45775  isomushgr  46480  mof02  47458  mofsn2  47464  mofeu  47467  fdomne0  47469  f002  47473  fullthinc  47619