Theorem feq2 6635

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3905  ran crn 5624   Fn wfn 6481  ⟶wf 6482

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6489  df-f 6490

This theorem is referenced by:  feq23  6637  feq2d  6640  feq2i  6648  f00  6710  f0dom0  6712  f1eq2  6720  fressnfv  7098  poseq  8098  soseq  8099  mapvalg  8770  fsetexb  8798  map0g  8818  ac6sfi  9189  cofsmo  10182  axcc4dom  10354  ac6sg  10401  isghm  19112  isghmOLD  19113  pjdm2  21636  cmpcovf  23294  ulmval  26305  elno2  27582  noreson  27588  measval  34167  isrnmeas  34169  bj-finsumval0  37261  mbfresfi  37648  sn-isghm  42649  dfno2  43404  relpeq4  44924  stoweidlem62  46047  hoidmvval0b  46575  vonioo  46667  vonicc  46670  f102g  48840  f1mo  48841