Theorem feq2 6689

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ⊆ wss 3895  ran crn 5651   Fn wfn 6534  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-fn 6542  df-f 6543

This theorem is used by:  feq23  6691  feq2d  6694  feq2i  6702  f00  6765  f0dom0  6767  f1eq2  6775  fressnfv  7165  poseq  8178  soseq  8179  mapvalg  8860  fsetexb  8890  map0g  8916  ac6sfi  9279  cofsmo  10351  axcc4dom  10523  ac6sg  10570  isghm  19436  pjdm2  22023  cmpcovf  23715  ulmval  26713  elno2  28017  noreson  28023  measval  34878  isrnmeas  34880  bj-finsumval0  38300  mbfresfi  38678  sn-isghm  43778  dfno2  44523  relpeq4  46031  stoweidlem62  47166  hoidmvval0b  47694  vonioo  47786  vonicc  47789  f102g  50057  f1mo  50058