Theorem feq2 6686

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ⊆ wss 3906  ran crn 5664   Fn wfn 6533  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-fn 6541  df-f 6542

This theorem is referenced by:  feq23  6688  feq2d  6691  feq2i  6699  f00  6762  f0dom0  6764  f1eq2  6772  fressnfv  7159  poseq  8155  soseq  8156  mapvalg  8834  fsetexb  8862  map0g  8883  ac6sfi  9245  cofsmo  10254  axcc4dom  10426  ac6sg  10473  isghm  19287  pjdm2  21842  cmpcovf  23529  ulmval  26524  elno2  27799  noreson  27805  measval  34569  isrnmeas  34571  bj-finsumval0  37910  mbfresfi  38298  sn-isghm  43388  dfno2  44137  relpeq4  45639  stoweidlem62  46759  hoidmvval0b  47287  vonioo  47379  vonicc  47382  f102g  49613  f1mo  49614