Theorem feq3d 6692

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ⟶wf 6526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943  df-f 6534

This theorem is referenced by:  feq123d  6694  fsn2  7125  fsng  7126  fsnunf  7176  funcres2b  17908  funcres2  17909  funcres2c  17914  catciso  18122  hofcl  18269  yonedalem4c  18287  yonedalem3b  18289  yonedainv  18291  gsumress  18658  resmgmhm2b  18689  resmhm2b  18798  pwsdiagmhm  18807  frmdup3lem  18842  frmdup3  18843  isghmOLD  19197  frgpup3lem  19756  gsumzsubmcl  19897  dmdprd  19979  zrtermorngc  20601  zrtermoringc  20633  imadrhmcl  20755  rngqiprngghm  21258  frlmup2  21757  scmatghm  22469  scmatmhm  22470  mdetdiaglem  22534  cnpf2  23186  2ndcctbss  23391  1stcelcls  23397  uptx  23561  txcn  23562  tsmssubm  24079  cnextucn  24239  pi1addf  24996  caufval  25225  equivcau  25250  lmcau  25263  plypf1  26167  coef2  26186  ulmval  26339  uhgr0vb  28997  uhgrun  28999  uhgrstrrepe  29003  isumgrs  29021  upgrun  29043  umgrun  29045  wksfval  29535  wlkres  29596  ajfval  30736  chscllem4  31567  feq3dd  32547  rlocf1  33214  imasmhm  33315  imasghm  33316  imasrhm  33317  lindfpropd  33343  ply1degltdimlem  33608  fedgmullem1  33615  rrhf  33975  sibff  34314  sibfof  34318  orvcval4  34439  bj-finsumval0  37249  matunitlindflem2  37587  poimirlem9  37599  isbnd3  37754  prdsbnd  37763  heibor  37791  elghomlem1OLD  37855  aks6d1c6lem2  42130  aks6d1c6lem3  42131  aks6d1c6isolem2  42134  aks6d1c6lem5  42136  evlsvvval  42533  cnfsmf  46717  upwlksfval  48058