Theorem feq2 6612

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1539   ⊆ wss 3892  ran crn 5601   Fn wfn 6453  ⟶wf 6454

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-fn 6461  df-f 6462

This theorem is referenced by:  feq23  6614  feq2d  6616  feq2i  6622  f00  6686  f0dom0  6688  f1eq2  6696  fressnfv  7064  mapvalg  8656  fsetexb  8683  map0g  8703  ac6sfi  9102  cofsmo  10071  axcc4dom  10243  ac6sg  10290  isghm  18879  pjdm2  20963  cmpcovf  22587  ulmval  25584  measval  32211  isrnmeas  32213  poseq  33847  soseq  33848  elno2  33902  noreson  33908  bj-finsumval0  35500  mbfresfi  35867  stoweidlem62  43652  hoidmvval0b  44178  vonioo  44270  vonicc  44273  f102g  46237  f1mo  46238