Theorem feq3 6700

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540   ⊆ wss 3948  ran crn 5677   Fn wfn 6538  ⟶wf 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-f 6547

This theorem is referenced by:  feq23  6701  feq3d  6704  fun2  6754  fconstg  6778  f1eq3  6784  mapvalg  8836  mapsnd  8886  cantnff  9675  axdc4uz  13956  supcvg  15809  lmff  23125  txcn  23450  lmmbr  25106  iscmet3  25141  dvcnvrelem2  25871  itgsubstlem  25903  umgrislfupgr  28817  usgrislfuspgr  28878  wlkv0  29342  isgrpo  30184  vciOLD  30248  isvclem  30264  nmop0h  31678  sitgaddlemb  33812  sitmcl  33815  cvmliftlem15  34754  mtyf  35008  matunitlindflem1  36950  sdclem1  37077  k0004lem1  43363  stoweidlem57  45234  f1ocof1ob  46250  isomushgr  46955  mof02  47669  mofsn2  47675  mofeu  47678  fdomne0  47680  f002  47684  fullthinc  47830