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 18	1 ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923  df-f 6542

This theorem is referenced by:  feq3dd  6694  feq123d  6696  fsn2  7134  fsng  7135  fsnunf  7185  funcres2b  17955  funcres2  17956  funcres2c  17961  catciso  18169  hofcl  18316  yonedalem4c  18334  yonedalem3b  18336  yonedainv  18338  gsumress  18741  resmgmhm2b  18772  resmhm2b  18882  pwsdiagmhm  18891  frmdup3lem  18926  frmdup3  18927  frgpup3lem  19848  gsumzsubmcl  19989  dmdprd  20071  zrtermorngc  20729  zrtermoringc  20761  imadrhmcl  20881  rngqiprngghm  21420  frlmup2  21930  evlsvvval  22225  scmatghm  22671  scmatmhm  22672  mdetdiaglem  22736  cnpf2  23388  2ndcctbss  23593  1stcelcls  23599  uptx  23763  txcn  23764  tsmssubm  24281  cnextucn  24440  pi1addf  25187  caufval  25415  equivcau  25440  lmcau  25453  plypf1  26350  coef2  26369  ulmval  26521  uhgr0vb  29400  uhgrun  29402  uhgrstrrepe  29406  isumgrs  29424  upgrun  29446  umgrun  29448  wksfval  29937  wlkres  29996  ajfval  31139  chscllem4  31970  rlocf1  33572  imasmhm  33652  imasghm  33653  imasrhm  33654  lindfpropd  33673  ply1degltdimlem  33990  fedgmullem1  33997  rrhf  34366  sibff  34704  sibfof  34708  orvcval4  34829  bj-finsumval0  37907  matunitlindflem2  38246  poimirlem9  38258  isbnd3  38413  prdsbnd  38422  heibor  38450  elghomlem1OLD  38514  aks6d1c6lem2  42916  aks6d1c6lem3  42917  aks6d1c6isolem2  42920  aks6d1c6lem5  42922  cnfsmf  47434  upwlksfval  48877