Theorem feq3d 6641

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

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

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922  df-f 6490

This theorem is referenced by:  feq3dd  6643  feq123d  6645  fsn2  7074  fsng  7075  fsnunf  7125  funcres2b  17822  funcres2  17823  funcres2c  17828  catciso  18036  hofcl  18183  yonedalem4c  18201  yonedalem3b  18203  yonedainv  18205  gsumress  18574  resmgmhm2b  18605  resmhm2b  18714  pwsdiagmhm  18723  frmdup3lem  18758  frmdup3  18759  isghmOLD  19113  frgpup3lem  19674  gsumzsubmcl  19815  dmdprd  19897  zrtermorngc  20546  zrtermoringc  20578  imadrhmcl  20700  rngqiprngghm  21224  frlmup2  21724  scmatghm  22436  scmatmhm  22437  mdetdiaglem  22501  cnpf2  23153  2ndcctbss  23358  1stcelcls  23364  uptx  23528  txcn  23529  tsmssubm  24046  cnextucn  24206  pi1addf  24963  caufval  25191  equivcau  25216  lmcau  25229  plypf1  26133  coef2  26152  ulmval  26305  uhgr0vb  29035  uhgrun  29037  uhgrstrrepe  29041  isumgrs  29059  upgrun  29081  umgrun  29083  wksfval  29573  wlkres  29632  ajfval  30771  chscllem4  31602  rlocf1  33223  imasmhm  33301  imasghm  33302  imasrhm  33303  lindfpropd  33329  ply1degltdimlem  33594  fedgmullem1  33601  rrhf  33964  sibff  34303  sibfof  34307  orvcval4  34428  bj-finsumval0  37258  matunitlindflem2  37596  poimirlem9  37608  isbnd3  37763  prdsbnd  37772  heibor  37800  elghomlem1OLD  37864  aks6d1c6lem2  42144  aks6d1c6lem3  42145  aks6d1c6isolem2  42148  aks6d1c6lem5  42150  evlsvvval  42536  cnfsmf  46722  upwlksfval  48120