Theorem feq3d 6637

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

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

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 3920  df-f 6486

This theorem is referenced by:  feq3dd  6639  feq123d  6641  fsn2  7070  fsng  7071  fsnunf  7121  funcres2b  17804  funcres2  17805  funcres2c  17810  catciso  18018  hofcl  18165  yonedalem4c  18183  yonedalem3b  18185  yonedainv  18187  gsumress  18556  resmgmhm2b  18587  resmhm2b  18696  pwsdiagmhm  18705  frmdup3lem  18740  frmdup3  18741  isghmOLD  19095  frgpup3lem  19656  gsumzsubmcl  19797  dmdprd  19879  zrtermorngc  20528  zrtermoringc  20560  imadrhmcl  20682  rngqiprngghm  21206  frlmup2  21706  scmatghm  22418  scmatmhm  22419  mdetdiaglem  22483  cnpf2  23135  2ndcctbss  23340  1stcelcls  23346  uptx  23510  txcn  23511  tsmssubm  24028  cnextucn  24188  pi1addf  24945  caufval  25173  equivcau  25198  lmcau  25211  plypf1  26115  coef2  26134  ulmval  26287  uhgr0vb  29021  uhgrun  29023  uhgrstrrepe  29027  isumgrs  29045  upgrun  29067  umgrun  29069  wksfval  29559  wlkres  29618  ajfval  30757  chscllem4  31588  rlocf1  33222  imasmhm  33300  imasghm  33301  imasrhm  33302  lindfpropd  33328  ply1degltdimlem  33605  fedgmullem1  33612  rrhf  33981  sibff  34320  sibfof  34324  orvcval4  34445  bj-finsumval0  37279  matunitlindflem2  37617  poimirlem9  37629  isbnd3  37784  prdsbnd  37793  heibor  37821  elghomlem1OLD  37885  aks6d1c6lem2  42164  aks6d1c6lem3  42165  aks6d1c6isolem2  42168  aks6d1c6lem5  42170  evlsvvval  42556  cnfsmf  46741  upwlksfval  48139