Theorem feq2 6696

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ⊆ wss 3947  ran crn 5676   Fn wfn 6535  ⟶wf 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6543  df-f 6544

This theorem is referenced by:  feq23  6698  feq2d  6700  feq2i  6706  f00  6770  f0dom0  6772  f1eq2  6780  fressnfv  7153  poseq  8139  soseq  8140  mapvalg  8826  fsetexb  8854  map0g  8874  ac6sfi  9283  cofsmo  10260  axcc4dom  10432  ac6sg  10479  isghm  19086  pjdm2  21250  cmpcovf  22877  ulmval  25874  elno2  27137  noreson  27143  measval  33134  isrnmeas  33136  bj-finsumval0  36104  mbfresfi  36472  dfno2  42112  stoweidlem62  44713  hoidmvval0b  45241  vonioo  45333  vonicc  45336  f102g  47420  f1mo  47421