Theorem feq3 6497

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ⊆ wss 3936  ran crn 5556   Fn wfn 6350  ⟶wf 6351

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-f 6359

This theorem is referenced by:  feq23  6498  feq3d  6501  fun2  6541  fconstg  6566  f1eq3  6572  mapvalg  8416  mapsnd  8450  cantnff  9137  axdc4uz  13353  supcvg  15211  lmff  21909  txcn  22234  lmmbr  23861  iscmet3  23896  dvcnvrelem2  24615  itgsubstlem  24645  umgrislfupgr  26908  usgrislfuspgr  26969  wlkv0  27432  isgrpo  28274  vciOLD  28338  isvclem  28354  nmop0h  29768  sitgaddlemb  31606  sitmcl  31609  cvmliftlem15  32545  mtyf  32799  matunitlindflem1  34903  sdclem1  35033  k0004lem1  40517  stoweidlem57  42362  isomushgr  44011