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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ⊆ wss 3890  ran crn 5626   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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-fn 6495  df-f 6496

This theorem is referenced by:  feq23  6643  feq2d  6646  feq2i  6654  f00  6716  f0dom0  6718  f1eq2  6726  fressnfv  7110  poseq  8105  soseq  8106  mapvalg  8780  fsetexb  8808  map0g  8829  ac6sfi  9191  cofsmo  10189  axcc4dom  10361  ac6sg  10408  isghm  19188  isghmOLD  19189  pjdm2  21693  cmpcovf  23381  ulmval  26370  elno2  27643  noreson  27649  measval  34389  isrnmeas  34391  bj-finsumval0  37652  mbfresfi  38040  sn-isghm  43130  dfno2  43879  relpeq4  45398  stoweidlem62  46512  hoidmvval0b  47040  vonioo  47132  vonicc  47135  f102g  49349  f1mo  49350