Theorem feq2 6498

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ⊆ wss 3938  ran crn 5558   Fn wfn 6352  ⟶wf 6353

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-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-fn 6360  df-f 6361

This theorem is referenced by:  feq23  6500  feq2d  6502  feq2i  6508  f00  6563  f0dom0  6565  f1eq2  6573  fressnfv  6924  mapvalg  8418  map0g  8450  ac6sfi  8764  cofsmo  9693  axcc4dom  9865  ac6sg  9912  isghm  18360  pjdm2  20857  cmpcovf  22001  ulmval  24970  measval  31459  isrnmeas  31461  poseq  33097  soseq  33098  elno2  33163  noreson  33169  bj-finsumval0  34569  mbfresfi  34940  stoweidlem62  42354  hoidmvval0b  42879  vonioo  42971  vonicc  42974