Theorem feq2 6700

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ⊆ wss 3949  ran crn 5678   Fn wfn 6539  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6547  df-f 6548

This theorem is referenced by:  feq23  6702  feq2d  6704  feq2i  6710  f00  6774  f0dom0  6776  f1eq2  6784  fressnfv  7158  poseq  8144  soseq  8145  mapvalg  8830  fsetexb  8858  map0g  8878  ac6sfi  9287  cofsmo  10264  axcc4dom  10436  ac6sg  10483  isghm  19092  pjdm2  21266  cmpcovf  22895  ulmval  25892  elno2  27157  noreson  27163  measval  33196  isrnmeas  33198  bj-finsumval0  36166  mbfresfi  36534  dfno2  42179  stoweidlem62  44778  hoidmvval0b  45306  vonioo  45398  vonicc  45401  f102g  47518  f1mo  47519