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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ⊆ wss 3890  ran crn 5625   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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6495  df-f 6496

This theorem is referenced by:  feq23  6643  feq2d  6646  feq2i  6654  f00  6716  f0dom0  6718  f1eq2  6726  fressnfv  7107  poseq  8101  soseq  8102  mapvalg  8776  fsetexb  8804  map0g  8825  ac6sfi  9187  cofsmo  10182  axcc4dom  10354  ac6sg  10401  isghm  19181  isghmOLD  19182  pjdm2  21701  cmpcovf  23366  ulmval  26358  elno2  27632  noreson  27638  measval  34358  isrnmeas  34360  bj-finsumval0  37615  mbfresfi  38001  sn-isghm  43120  dfno2  43873  relpeq4  45392  stoweidlem62  46508  hoidmvval0b  47036  vonioo  47128  vonicc  47131  f102g  49339  f1mo  49340