Theorem feq2 6670

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3917  ran crn 5642   Fn wfn 6509  ⟶wf 6510

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 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-fn 6517  df-f 6518

This theorem is referenced by:  feq23  6672  feq2d  6675  feq2i  6683  f00  6745  f0dom0  6747  f1eq2  6755  fressnfv  7135  poseq  8140  soseq  8141  mapvalg  8812  fsetexb  8840  map0g  8860  ac6sfi  9238  cofsmo  10229  axcc4dom  10401  ac6sg  10448  isghm  19154  isghmOLD  19155  pjdm2  21627  cmpcovf  23285  ulmval  26296  elno2  27573  noreson  27579  measval  34195  isrnmeas  34197  bj-finsumval0  37280  mbfresfi  37667  sn-isghm  42668  dfno2  43424  relpeq4  44944  stoweidlem62  46067  hoidmvval0b  46595  vonioo  46687  vonicc  46690  f102g  48844  f1mo  48845