Theorem feq3d 6503

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ⟶wf 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954  df-f 6361

This theorem is referenced by:  feq123d  6505  fsn2  6900  fsng  6901  fsnunf  6949  funcres2b  17169  funcres2  17170  funcres2c  17173  catciso  17369  hofcl  17511  yonedalem4c  17529  yonedalem3b  17531  yonedainv  17533  gsumress  17894  resmhm2b  17989  pwsdiagmhm  17997  frmdup3lem  18033  frmdup3  18034  isghm  18360  frgpup3lem  18905  gsumzsubmcl  19040  dmdprd  19122  frlmup2  20945  scmatghm  21144  scmatmhm  21145  mdetdiaglem  21209  cnpf2  21860  2ndcctbss  22065  1stcelcls  22071  uptx  22235  txcn  22236  tsmssubm  22753  cnextucn  22914  pi1addf  23653  caufval  23880  equivcau  23905  lmcau  23918  plypf1  24804  coef2  24823  ulmval  24970  uhgr0vb  26859  uhgrun  26861  uhgrstrrepe  26865  isumgrs  26883  upgrun  26905  umgrun  26907  wksfval  27393  wlkres  27454  ajfval  28588  chscllem4  29419  lindfpropd  30944  fedgmullem1  31027  rrhf  31241  sibff  31596  sibfof  31600  orvcval4  31720  bj-finsumval0  34569  matunitlindflem2  34891  poimirlem9  34903  isbnd3  35064  prdsbnd  35073  heibor  35101  elghomlem1OLD  35165  selvval2lem4  39143  cnfsmf  43024  upwlksfval  44017  resmgmhm2b  44074  zrtermorngc  44279  zrtermoringc  44348