Theorem feq3d 6723

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-f 6565

This theorem is referenced by:  feq123d  6725  fsn2  7156  fsng  7157  fsnunf  7205  funcres2b  17942  funcres2  17943  funcres2c  17948  catciso  18156  hofcl  18304  yonedalem4c  18322  yonedalem3b  18324  yonedainv  18326  gsumress  18695  resmgmhm2b  18726  resmhm2b  18835  pwsdiagmhm  18844  frmdup3lem  18879  frmdup3  18880  isghmOLD  19234  frgpup3lem  19795  gsumzsubmcl  19936  dmdprd  20018  zrtermorngc  20643  zrtermoringc  20675  imadrhmcl  20798  rngqiprngghm  21309  frlmup2  21819  scmatghm  22539  scmatmhm  22540  mdetdiaglem  22604  cnpf2  23258  2ndcctbss  23463  1stcelcls  23469  uptx  23633  txcn  23634  tsmssubm  24151  cnextucn  24312  pi1addf  25080  caufval  25309  equivcau  25334  lmcau  25347  plypf1  26251  coef2  26270  ulmval  26423  uhgr0vb  29089  uhgrun  29091  uhgrstrrepe  29095  isumgrs  29113  upgrun  29135  umgrun  29137  wksfval  29627  wlkres  29688  ajfval  30828  chscllem4  31659  feq3dd  32633  rlocf1  33277  imasmhm  33382  imasghm  33383  imasrhm  33384  lindfpropd  33410  ply1degltdimlem  33673  fedgmullem1  33680  rrhf  33999  sibff  34338  sibfof  34342  orvcval4  34463  bj-finsumval0  37286  matunitlindflem2  37624  poimirlem9  37636  isbnd3  37791  prdsbnd  37800  heibor  37828  elghomlem1OLD  37892  aks6d1c6lem2  42172  aks6d1c6lem3  42173  aks6d1c6isolem2  42176  aks6d1c6lem5  42178  evlsvvval  42573  cnfsmf  46755  upwlksfval  48051