Theorem feq3d 6691

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919  df-f 6541

This theorem is used by:  feq3dd  6693  feq123d  6695  fsn2  7134  fsng  7135  fsnunf  7187  funcres2b  17992  funcres2  17993  funcres2c  17998  catciso  18206  hofcl  18353  yonedalem4c  18371  yonedalem3b  18373  yonedainv  18375  gsumress  18790  resmgmhm2b  18821  resmhm2b  18937  pwsdiagmhm  18946  frmdup3lem  18981  frmdup3  18982  frgpup3lem  19910  gsumzsubmcl  20051  dmdprd  20133  zrtermorngc  20811  zrtermoringc  20843  imadrhmcl  20969  rngqiprngghm  21508  frlmup2  22018  evlsvvval  22315  scmatghm  22761  scmatmhm  22762  mdetdiaglem  22826  matunitlindflem2  22908  cnpf2  23481  2ndcctbss  23687  1stcelcls  23693  uptx  23857  txcn  23858  tsmssubm  24375  cnextucn  24534  pi1addf  25281  caufval  25509  equivcau  25534  lmcau  25547  plypf1  26445  coef2  26464  ulmval  26623  uhgr0vb  29537  uhgrun  29539  uhgrstrrepe  29543  isumgrs  29561  upgrun  29583  umgrun  29585  wksfval  30077  wlkres  30136  ajfval  31298  chscllem4  32129  rlocf1  33722  imasmhm  33802  imasghm  33803  imasrhm  33804  lindfpropd  33823  ply1degltdimlem  34140  fedgmullem1  34147  rrhf  34516  sibff  34855  sibfof  34859  orvcval4  34980  bj-finsumval0  38045  poimirlem9  38386  isbnd3  38542  prdsbnd  38551  heibor  38579  elghomlem1OLD  38643  aks6d1c6lem2  43045  aks6d1c6lem3  43046  aks6d1c6isolem2  43049  aks6d1c6lem5  43051  cnfsmf  47576  upwlksfval  49059