Theorem feq2 6647

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ⊆ wss 3889  ran crn 5632   Fn wfn 6493  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-fn 6501  df-f 6502

This theorem is referenced by:  feq23  6649  feq2d  6652  feq2i  6660  f00  6722  f0dom0  6724  f1eq2  6732  fressnfv  7114  poseq  8108  soseq  8109  mapvalg  8783  fsetexb  8811  map0g  8832  ac6sfi  9194  cofsmo  10191  axcc4dom  10363  ac6sg  10410  isghm  19190  isghmOLD  19191  pjdm2  21691  cmpcovf  23356  ulmval  26345  elno2  27618  noreson  27624  measval  34342  isrnmeas  34344  bj-finsumval0  37599  mbfresfi  37987  sn-isghm  43106  dfno2  43855  relpeq4  45374  stoweidlem62  46490  hoidmvval0b  47018  vonioo  47110  vonicc  47113  f102g  49327  f1mo  49328