Theorem feq3d 6032

Description: Equality deduction for functions. (Contributed by AV, 1-Jan-2020.)

Hypothesis

Ref	Expression
feq2d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
feq3d	|- ( ph -> ( F : X --> A <-> F : X --> B ) )

Proof of Theorem feq3d

Step	Hyp	Ref	Expression
1		feq2d.1	. 2 |- ( ph -> A = B )
2		feq3 6028	. 2 |- ( A = B -> ( F : X --> A <-> F : X --> B ) )
3	1, 2	syl 17	1 |- ( ph -> ( F : X --> A <-> F : X --> B ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   -->wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-f 5892

This theorem is referenced by:  feq123d  6034  fsn2  6403  fsng  6404  fsnunf  6451  funcres2b  16557  funcres2  16558  funcres2c  16561  catciso  16757  hofcl  16899  yonedalem4c  16917  yonedalem3b  16919  yonedainv  16921  gsumress  17276  resmhm2b  17361  pwsdiagmhm  17369  frmdup3lem  17403  frmdup3  17404  isghm  17660  frgpup3lem  18190  gsumzsubmcl  18318  dmdprd  18397  frlmup2  20138  scmatghm  20339  scmatmhm  20340  mdetdiaglem  20404  cnpf2  21054  2ndcctbss  21258  1stcelcls  21264  uptx  21428  txcn  21429  tsmssubm  21946  cnextucn  22107  pi1addf  22847  caufval  23073  equivcau  23098  lmcau  23111  plypf1  23968  coef2  23987  ulmval  24134  uhgr0vb  25967  uhgrun  25969  uhgrstrrepe  25973  isumgrs  25991  upgrun  26013  umgrun  26015  wksfval  26505  wlkres  26567  ajfval  27664  chscllem4  28499  rrhf  30042  sibff  30398  sibfof  30402  orvcval4  30522  bj-finsumval0  33147  matunitlindflem2  33406  poimirlem9  33418  isbnd3  33583  prdsbnd  33592  heibor  33620  elghomlem1OLD  33684  cnfsmf  40949  upwlksfval  41716  resmgmhm2b  41800  zrtermorngc  42001  zrtermoringc  42070