Theorem feq3d 6647

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 6642	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ⟶wf 6488

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-ss 3907  df-f 6496

This theorem is referenced by:  feq3dd  6649  feq123d  6651  fsn2  7083  fsng  7084  fsnunf  7133  funcres2b  17855  funcres2  17856  funcres2c  17861  catciso  18069  hofcl  18216  yonedalem4c  18234  yonedalem3b  18236  yonedainv  18238  gsumress  18641  resmgmhm2b  18672  resmhm2b  18781  pwsdiagmhm  18790  frmdup3lem  18825  frmdup3  18826  isghmOLD  19182  frgpup3lem  19743  gsumzsubmcl  19884  dmdprd  19966  zrtermorngc  20611  zrtermoringc  20643  imadrhmcl  20765  rngqiprngghm  21289  frlmup2  21789  evlsvvval  22081  scmatghm  22508  scmatmhm  22509  mdetdiaglem  22573  cnpf2  23225  2ndcctbss  23430  1stcelcls  23436  uptx  23600  txcn  23601  tsmssubm  24118  cnextucn  24277  pi1addf  25024  caufval  25252  equivcau  25277  lmcau  25290  plypf1  26187  coef2  26206  ulmval  26358  uhgr0vb  29155  uhgrun  29157  uhgrstrrepe  29161  isumgrs  29179  upgrun  29201  umgrun  29203  wksfval  29693  wlkres  29752  ajfval  30895  chscllem4  31726  rlocf1  33349  imasmhm  33429  imasghm  33430  imasrhm  33431  lindfpropd  33457  ply1degltdimlem  33782  fedgmullem1  33789  rrhf  34158  sibff  34496  sibfof  34500  orvcval4  34621  bj-finsumval0  37615  matunitlindflem2  37952  poimirlem9  37964  isbnd3  38119  prdsbnd  38128  heibor  38156  elghomlem1OLD  38220  aks6d1c6lem2  42624  aks6d1c6lem3  42625  aks6d1c6isolem2  42628  aks6d1c6lem5  42630  cnfsmf  47186  upwlksfval  48623