Theorem feq3d 6710

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  ⟶wf 6545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ss 3961  df-f 6553

This theorem is referenced by:  feq123d  6712  fsn2  7145  fsng  7146  fsnunf  7194  funcres2b  17886  funcres2  17887  funcres2c  17893  catciso  18103  hofcl  18254  yonedalem4c  18272  yonedalem3b  18274  yonedainv  18276  gsumress  18645  resmgmhm2b  18676  resmhm2b  18782  pwsdiagmhm  18791  frmdup3lem  18826  frmdup3  18827  isghmOLD  19179  frgpup3lem  19744  gsumzsubmcl  19885  dmdprd  19967  zrtermorngc  20588  zrtermoringc  20620  imadrhmcl  20697  rngqiprngghm  21206  frlmup2  21750  scmatghm  22479  scmatmhm  22480  mdetdiaglem  22544  cnpf2  23198  2ndcctbss  23403  1stcelcls  23409  uptx  23573  txcn  23574  tsmssubm  24091  cnextucn  24252  pi1addf  25018  caufval  25247  equivcau  25272  lmcau  25285  plypf1  26191  coef2  26210  ulmval  26361  uhgr0vb  28957  uhgrun  28959  uhgrstrrepe  28963  isumgrs  28981  upgrun  29003  umgrun  29005  wksfval  29495  wlkres  29556  ajfval  30691  chscllem4  31522  feq3dd  32490  rlocf1  33063  imasmhm  33165  imasghm  33166  imasrhm  33167  lindfpropd  33194  ply1degltdimlem  33448  fedgmullem1  33455  rrhf  33727  sibff  34084  sibfof  34088  orvcval4  34208  bj-finsumval0  36892  matunitlindflem2  37218  poimirlem9  37230  isbnd3  37385  prdsbnd  37394  heibor  37422  elghomlem1OLD  37486  aks6d1c6lem2  41771  aks6d1c6lem3  41772  aks6d1c6isolem2  41775  aks6d1c6lem5  41777  evlsvvval  41928  cnfsmf  46263  upwlksfval  47380