Theorem feq2 6688

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ⊆ wss 3906  ran crn 5664   Fn wfn 6535  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-fn 6543  df-f 6544

This theorem is used by:  feq23  6690  feq2d  6693  feq2i  6701  f00  6764  f0dom0  6766  f1eq2  6774  fressnfv  7161  poseq  8156  soseq  8157  mapvalg  8835  fsetexb  8863  map0g  8884  ac6sfi  9247  cofsmo  10264  axcc4dom  10436  ac6sg  10483  isghm  19309  pjdm2  21890  cmpcovf  23577  ulmval  26572  elno2  27847  noreson  27853  measval  34612  isrnmeas  34614  bj-finsumval0  37962  mbfresfi  38350  sn-isghm  43438  dfno2  44187  relpeq4  45689  stoweidlem62  46809  hoidmvval0b  47337  vonioo  47429  vonicc  47432  f102g  49663  f1mo  49664