Theorem feq2 6630

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ⊆ wss 3902  ran crn 5617   Fn wfn 6476  ⟶wf 6477

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 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-fn 6484  df-f 6485

This theorem is referenced by:  feq23  6632  feq2d  6635  feq2i  6643  f00  6705  f0dom0  6707  f1eq2  6715  fressnfv  7093  poseq  8088  soseq  8089  mapvalg  8760  fsetexb  8788  map0g  8808  ac6sfi  9168  cofsmo  10160  axcc4dom  10332  ac6sg  10379  isghm  19128  isghmOLD  19129  pjdm2  21649  cmpcovf  23307  ulmval  26317  elno2  27594  noreson  27600  measval  34209  isrnmeas  34211  bj-finsumval0  37325  mbfresfi  37712  sn-isghm  42712  dfno2  43467  relpeq4  44986  stoweidlem62  46106  hoidmvval0b  46634  vonioo  46726  vonicc  46729  f102g  48889  f1mo  48890