Theorem feq3d 6680

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924  df-f 6529

This theorem is referenced by:  feq3dd  6682  feq123d  6684  fsn2  7122  fsng  7123  fsnunf  7173  funcres2b  17944  funcres2  17945  funcres2c  17950  catciso  18158  hofcl  18305  yonedalem4c  18323  yonedalem3b  18325  yonedainv  18327  gsumress  18730  resmgmhm2b  18761  resmhm2b  18871  pwsdiagmhm  18880  frmdup3lem  18915  frmdup3  18916  frgpup3lem  19838  gsumzsubmcl  19979  dmdprd  20061  zrtermorngc  20719  zrtermoringc  20751  imadrhmcl  20869  rngqiprngghm  21401  frlmup2  21909  evlsvvval  22204  scmatghm  22651  scmatmhm  22652  mdetdiaglem  22716  cnpf2  23368  2ndcctbss  23573  1stcelcls  23579  uptx  23743  txcn  23744  tsmssubm  24261  cnextucn  24420  pi1addf  25167  caufval  25395  equivcau  25420  lmcau  25433  plypf1  26330  coef2  26349  ulmval  26501  uhgr0vb  29331  uhgrun  29333  uhgrstrrepe  29337  isumgrs  29355  upgrun  29377  umgrun  29379  wksfval  29868  wlkres  29927  ajfval  31070  chscllem4  31901  rlocf1  33507  imasmhm  33589  imasghm  33590  imasrhm  33591  lindfpropd  33611  ply1degltdimlem  33929  fedgmullem1  33936  rrhf  34305  sibff  34643  sibfof  34647  orvcval4  34768  bj-finsumval0  37789  matunitlindflem2  38128  poimirlem9  38140  isbnd3  38295  prdsbnd  38304  heibor  38332  elghomlem1OLD  38396  aks6d1c6lem2  42800  aks6d1c6lem3  42801  aks6d1c6isolem2  42804  aks6d1c6lem5  42806  cnfsmf  47312  upwlksfval  48755