Theorem feq3d 6704

Description: Equality deduction for functions. (Contributed by AV, 1-Jan-2020.)

Hypothesis

Ref	Expression
feq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
feq3d	⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))

Proof of Theorem feq3d

Step	Hyp	Ref	Expression
1		feq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		feq3 6700	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ⟶wf 6539

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-f 6547

This theorem is referenced by:  feq123d  6706  fsn2  7133  fsng  7134  fsnunf  7182  funcres2b  17846  funcres2  17847  funcres2c  17851  catciso  18060  hofcl  18211  yonedalem4c  18229  yonedalem3b  18231  yonedainv  18233  gsumress  18600  resmhm2b  18702  pwsdiagmhm  18711  frmdup3lem  18746  frmdup3  18747  isghm  19091  frgpup3lem  19644  gsumzsubmcl  19785  dmdprd  19867  imadrhmcl  20412  frlmup2  21353  scmatghm  22034  scmatmhm  22035  mdetdiaglem  22099  cnpf2  22753  2ndcctbss  22958  1stcelcls  22964  uptx  23128  txcn  23129  tsmssubm  23646  cnextucn  23807  pi1addf  24562  caufval  24791  equivcau  24816  lmcau  24829  plypf1  25725  coef2  25744  ulmval  25891  uhgr0vb  28329  uhgrun  28331  uhgrstrrepe  28335  isumgrs  28353  upgrun  28375  umgrun  28377  wksfval  28863  wlkres  28924  ajfval  30057  chscllem4  30888  lindfpropd  32493  ply1degltdimlem  32702  fedgmullem1  32709  rrhf  32973  sibff  33330  sibfof  33334  orvcval4  33454  bj-finsumval0  36161  matunitlindflem2  36480  poimirlem9  36492  isbnd3  36647  prdsbnd  36656  heibor  36684  elghomlem1OLD  36748  evlsvvval  41137  cnfsmf  45446  upwlksfval  46503  resmgmhm2b  46560  rngqiprngghm  46774  zrtermorngc  46889  zrtermoringc  46958