Theorem funeqd 6371

Description: Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)

Hypothesis

Ref	Expression
funeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
funeqd	⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))

Proof of Theorem funeqd

Step	Hyp	Ref	Expression
1		funeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		funeq 6369	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533  Fun wfun 6343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3942  df-ss 3951  df-br 5059  df-opab 5121  df-rel 5556  df-cnv 5557  df-co 5558  df-fun 6351

This theorem is referenced by:  funopg  6383  funsng  6399  f1eq1  6564  f1ssf1  6640  fvn0ssdmfun  6836  funcnvuni  7630  fundmge2nop0  13844  funcnvs2  14269  funcnvs3  14270  funcnvs4  14271  shftfn  14426  isstruct2  16487  structfung  16492  setsfun  16512  setsfun0  16513  strle1  16586  monfval  16996  ismon  16997  monpropd  17001  isepi  17004  isfth  17178  estrres  17383  lubfun  17584  glbfun  17597  acsficl2d  17780  frlmphl  20919  ebtwntg  26762  ecgrtg  26763  elntg  26764  uhgrspansubgrlem  27066  istrl  27472  ispth  27498  isspth  27499  upgrwlkdvspth  27514  uhgrwkspthlem1  27528  uhgrwkspthlem2  27529  usgr2wlkspthlem1  27532  usgr2wlkspthlem2  27533  pthdlem1  27541  2spthd  27714  0spth  27899  3spthd  27949  trlsegvdeglem2  27994  trlsegvdeglem3  27995  ajfun  28631  fresf1o  30370  padct  30449  smatrcl  31056  esum2dlem  31346  omssubadd  31553  sitgf  31600  funen1cnv  32352  pthhashvtx  32369  satfv0fun  32613  satffunlem1  32649  satffunlem2  32650  satffun  32651  satefvfmla0  32660  satefvfmla1  32667  fperdvper  42196  ovnovollem1  42932  funressnmo  43275  dfateq12d  43319  afvres  43365  funressndmafv2rn  43416  afv2res  43432  fdivval  44593