Theorem feq2 6505

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ⊆ wss 3853  ran crn 5537   Fn wfn 6353  ⟶wf 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-fn 6361  df-f 6362

This theorem is referenced by:  feq23  6507  feq2d  6509  feq2i  6515  f00  6579  f0dom0  6581  f1eq2  6589  fressnfv  6953  mapvalg  8496  fsetexb  8523  map0g  8543  ac6sfi  8893  cofsmo  9848  axcc4dom  10020  ac6sg  10067  isghm  18576  pjdm2  20627  cmpcovf  22242  ulmval  25226  measval  31832  isrnmeas  31834  poseq  33482  soseq  33483  elno2  33543  noreson  33549  bj-finsumval0  35140  mbfresfi  35509  stoweidlem62  43221  hoidmvval0b  43746  vonioo  43838  vonicc  43841  f102g  45795  f1mo  45796