Theorem feq2 6578

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1541   ⊆ wss 3891  ran crn 5589   Fn wfn 6425  ⟶wf 6426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-fn 6433  df-f 6434

This theorem is referenced by:  feq23  6580  feq2d  6582  feq2i  6588  f00  6652  f0dom0  6654  f1eq2  6662  fressnfv  7026  mapvalg  8599  fsetexb  8626  map0g  8646  ac6sfi  9019  cofsmo  10009  axcc4dom  10181  ac6sg  10228  isghm  18815  pjdm2  20899  cmpcovf  22523  ulmval  25520  measval  32145  isrnmeas  32147  poseq  33781  soseq  33782  elno2  33836  noreson  33842  bj-finsumval0  35435  mbfresfi  35802  stoweidlem62  43557  hoidmvval0b  44082  vonioo  44174  vonicc  44177  f102g  46131  f1mo  46132