Theorem feq3d 6734

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993  df-f 6577

This theorem is referenced by:  feq123d  6736  fsn2  7170  fsng  7171  fsnunf  7219  funcres2b  17961  funcres2  17962  funcres2c  17968  catciso  18178  hofcl  18329  yonedalem4c  18347  yonedalem3b  18349  yonedainv  18351  gsumress  18720  resmgmhm2b  18751  resmhm2b  18857  pwsdiagmhm  18866  frmdup3lem  18901  frmdup3  18902  isghmOLD  19256  frgpup3lem  19819  gsumzsubmcl  19960  dmdprd  20042  zrtermorngc  20665  zrtermoringc  20697  imadrhmcl  20820  rngqiprngghm  21332  frlmup2  21842  scmatghm  22560  scmatmhm  22561  mdetdiaglem  22625  cnpf2  23279  2ndcctbss  23484  1stcelcls  23490  uptx  23654  txcn  23655  tsmssubm  24172  cnextucn  24333  pi1addf  25099  caufval  25328  equivcau  25353  lmcau  25366  plypf1  26271  coef2  26290  ulmval  26441  uhgr0vb  29107  uhgrun  29109  uhgrstrrepe  29113  isumgrs  29131  upgrun  29153  umgrun  29155  wksfval  29645  wlkres  29706  ajfval  30841  chscllem4  31672  feq3dd  32643  rlocf1  33245  imasmhm  33347  imasghm  33348  imasrhm  33349  lindfpropd  33375  ply1degltdimlem  33635  fedgmullem1  33642  rrhf  33944  sibff  34301  sibfof  34305  orvcval4  34425  bj-finsumval0  37251  matunitlindflem2  37577  poimirlem9  37589  isbnd3  37744  prdsbnd  37753  heibor  37781  elghomlem1OLD  37845  aks6d1c6lem2  42128  aks6d1c6lem3  42129  aks6d1c6isolem2  42132  aks6d1c6lem5  42134  evlsvvval  42518  cnfsmf  46661  upwlksfval  47858