Theorem feq2 6665

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ⊆ wss 3902  ran crn 5644   Fn wfn 6511  ⟶wf 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-fn 6519  df-f 6520

This theorem is referenced by:  feq23  6667  feq2d  6670  feq2i  6678  f00  6741  f0dom0  6743  f1eq2  6751  fressnfv  7138  poseq  8132  soseq  8133  mapvalg  8811  fsetexb  8839  map0g  8860  ac6sfi  9222  cofsmo  10220  axcc4dom  10392  ac6sg  10439  isghm  19247  pjdm2  21751  cmpcovf  23439  ulmval  26431  elno2  27706  noreson  27712  measval  34456  isrnmeas  34458  bj-finsumval0  37738  mbfresfi  38126  sn-isghm  43216  dfno2  43965  relpeq4  45484  stoweidlem62  46597  hoidmvval0b  47125  vonioo  47217  vonicc  47220  f102g  49434  f1mo  49435