Theorem feq3d 6691

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ⟶wf 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930  df-f 6541

This theorem is referenced by:  feq3dd  6693  feq123d  6695  fsn2  7133  fsng  7134  fsnunf  7184  funcres2b  17953  funcres2  17954  funcres2c  17959  catciso  18167  hofcl  18314  yonedalem4c  18332  yonedalem3b  18334  yonedainv  18336  gsumress  18739  resmgmhm2b  18770  resmhm2b  18880  pwsdiagmhm  18889  frmdup3lem  18924  frmdup3  18925  frgpup3lem  19846  gsumzsubmcl  19987  dmdprd  20069  zrtermorngc  20727  zrtermoringc  20759  imadrhmcl  20877  rngqiprngghm  21409  frlmup2  21917  evlsvvval  22212  scmatghm  22658  scmatmhm  22659  mdetdiaglem  22723  cnpf2  23375  2ndcctbss  23580  1stcelcls  23586  uptx  23750  txcn  23751  tsmssubm  24268  cnextucn  24427  pi1addf  25174  caufval  25402  equivcau  25427  lmcau  25440  plypf1  26337  coef2  26356  ulmval  26508  uhgr0vb  29362  uhgrun  29364  uhgrstrrepe  29368  isumgrs  29386  upgrun  29408  umgrun  29410  wksfval  29899  wlkres  29958  ajfval  31101  chscllem4  31932  rlocf1  33534  imasmhm  33616  imasghm  33617  imasrhm  33618  lindfpropd  33638  ply1degltdimlem  33956  fedgmullem1  33963  rrhf  34332  sibff  34670  sibfof  34674  orvcval4  34795  bj-finsumval0  37816  matunitlindflem2  38155  poimirlem9  38167  isbnd3  38322  prdsbnd  38331  heibor  38359  elghomlem1OLD  38423  aks6d1c6lem2  42827  aks6d1c6lem3  42828  aks6d1c6isolem2  42831  aks6d1c6lem5  42833  cnfsmf  47345  upwlksfval  48788