Theorem feq2 6682

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ⊆ wss 3913  ran crn 5660   Fn wfn 6528  ⟶wf 6529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-fn 6536  df-f 6537

This theorem is referenced by:  feq23  6684  feq2d  6687  feq2i  6695  f00  6758  f0dom0  6760  f1eq2  6768  fressnfv  7155  poseq  8150  soseq  8151  mapvalg  8829  fsetexb  8857  map0g  8878  ac6sfi  9240  cofsmo  10249  axcc4dom  10421  ac6sg  10468  isghm  19282  pjdm2  21826  cmpcovf  23513  ulmval  26505  elno2  27780  noreson  27786  measval  34529  isrnmeas  34531  bj-finsumval0  37812  mbfresfi  38200  sn-isghm  43290  dfno2  44039  relpeq4  45541  stoweidlem62  46661  hoidmvval0b  47189  vonioo  47281  vonicc  47284  f102g  49508  f1mo  49509