Theorem feq2 6687

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3926  ran crn 5655   Fn wfn 6526  ⟶wf 6527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-fn 6534  df-f 6535

This theorem is referenced by:  feq23  6689  feq2d  6692  feq2i  6698  f00  6760  f0dom0  6762  f1eq2  6770  fressnfv  7150  poseq  8157  soseq  8158  mapvalg  8850  fsetexb  8878  map0g  8898  ac6sfi  9292  cofsmo  10283  axcc4dom  10455  ac6sg  10502  isghm  19198  isghmOLD  19199  pjdm2  21671  cmpcovf  23329  ulmval  26341  elno2  27618  noreson  27624  measval  34229  isrnmeas  34231  bj-finsumval0  37303  mbfresfi  37690  sn-isghm  42696  dfno2  43452  relpeq4  44972  stoweidlem62  46091  hoidmvval0b  46619  vonioo  46711  vonicc  46714  f102g  48830  f1mo  48831