Theorem feq2 6641

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ⊆ wss 3901  ran crn 5625   Fn wfn 6487  ⟶wf 6488

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-fn 6495  df-f 6496

This theorem is referenced by:  feq23  6643  feq2d  6646  feq2i  6654  f00  6716  f0dom0  6718  f1eq2  6726  fressnfv  7105  poseq  8100  soseq  8101  mapvalg  8773  fsetexb  8801  map0g  8822  ac6sfi  9184  cofsmo  10179  axcc4dom  10351  ac6sg  10398  isghm  19144  isghmOLD  19145  pjdm2  21666  cmpcovf  23335  ulmval  26345  elno2  27622  noreson  27628  measval  34355  isrnmeas  34357  bj-finsumval0  37490  mbfresfi  37867  sn-isghm  42916  dfno2  43669  relpeq4  45188  stoweidlem62  46306  hoidmvval0b  46834  vonioo  46926  vonicc  46929  f102g  49097  f1mo  49098