Theorem feq3d 6653

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-f 6502

This theorem is referenced by:  feq3dd  6655  feq123d  6657  fsn2  7089  fsng  7090  fsnunf  7140  funcres2b  17864  funcres2  17865  funcres2c  17870  catciso  18078  hofcl  18225  yonedalem4c  18243  yonedalem3b  18245  yonedainv  18247  gsumress  18650  resmgmhm2b  18681  resmhm2b  18790  pwsdiagmhm  18799  frmdup3lem  18834  frmdup3  18835  isghmOLD  19191  frgpup3lem  19752  gsumzsubmcl  19893  dmdprd  19975  zrtermorngc  20620  zrtermoringc  20652  imadrhmcl  20774  rngqiprngghm  21297  frlmup2  21779  evlsvvval  22071  scmatghm  22498  scmatmhm  22499  mdetdiaglem  22563  cnpf2  23215  2ndcctbss  23420  1stcelcls  23426  uptx  23590  txcn  23591  tsmssubm  24108  cnextucn  24267  pi1addf  25014  caufval  25242  equivcau  25267  lmcau  25280  plypf1  26177  coef2  26196  ulmval  26345  uhgr0vb  29141  uhgrun  29143  uhgrstrrepe  29147  isumgrs  29165  upgrun  29187  umgrun  29189  wksfval  29678  wlkres  29737  ajfval  30880  chscllem4  31711  rlocf1  33334  imasmhm  33414  imasghm  33415  imasrhm  33416  lindfpropd  33442  ply1degltdimlem  33766  fedgmullem1  33773  rrhf  34142  sibff  34480  sibfof  34484  orvcval4  34605  bj-finsumval0  37599  matunitlindflem2  37938  poimirlem9  37950  isbnd3  38105  prdsbnd  38114  heibor  38142  elghomlem1OLD  38206  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6isolem2  42614  aks6d1c6lem5  42616  cnfsmf  47168  upwlksfval  48611