Theorem feq2 6637

Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
feq2	⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))

Proof of Theorem feq2

Step	Hyp	Ref	Expression
1		fneq2 6580	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
2	1	anbi1d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶)))
3		df-f 6492	. 2 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
4		df-f 6492	. 2 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ⊆ wss 3898  ran crn 5622   Fn wfn 6483  ⟶wf 6484

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 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-fn 6491  df-f 6492

This theorem is referenced by:  feq23  6639  feq2d  6642  feq2i  6650  f00  6712  f0dom0  6714  f1eq2  6722  fressnfv  7101  poseq  8096  soseq  8097  mapvalg  8768  fsetexb  8796  map0g  8816  ac6sfi  9177  cofsmo  10169  axcc4dom  10341  ac6sg  10388  isghm  19131  isghmOLD  19132  pjdm2  21652  cmpcovf  23309  ulmval  26319  elno2  27596  noreson  27602  measval  34234  isrnmeas  34236  bj-finsumval0  37352  mbfresfi  37729  sn-isghm  42794  dfno2  43548  relpeq4  45067  stoweidlem62  46187  hoidmvval0b  46715  vonioo  46807  vonicc  46810  f102g  48979  f1mo  48980