Theorem feq2 6649

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ⊆ wss 3903  ran crn 5633   Fn wfn 6495  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6503  df-f 6504

This theorem is referenced by:  feq23  6651  feq2d  6654  feq2i  6662  f00  6724  f0dom0  6726  f1eq2  6734  fressnfv  7115  poseq  8110  soseq  8111  mapvalg  8785  fsetexb  8813  map0g  8834  ac6sfi  9196  cofsmo  10191  axcc4dom  10363  ac6sg  10410  isghm  19156  isghmOLD  19157  pjdm2  21678  cmpcovf  23347  ulmval  26357  elno2  27634  noreson  27640  measval  34375  isrnmeas  34377  bj-finsumval0  37537  mbfresfi  37914  sn-isghm  43028  dfno2  43781  relpeq4  45300  stoweidlem62  46417  hoidmvval0b  46945  vonioo  47037  vonicc  47040  f102g  49208  f1mo  49209