Theorem funeqd 6545

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 6543	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562  Fun wfun 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ss 3923  df-br 5103  df-opab 5165  df-rel 5656  df-cnv 5657  df-co 5658  df-fun 6525

This theorem is referenced by:  funopg  6557  funsng  6574  f1eq1  6757  f1ssf1  6841  fvn0ssdmfun  7057  funcnvuni  7915  fundmge2nop0  14517  funcnvs2  14928  funcnvs3  14929  funcnvs4  14930  shftfn  15088  isstruct2  17187  structfung  17192  strle1  17196  setsfun  17209  setsfun0  17210  monfval  17767  ismon  17768  monpropd  17772  isepi  17775  isfth  17951  estrres  18173  lubfun  18384  glbfun  18397  acsficl2d  18586  ebtwntg  29185  ecgrtg  29186  elntg  29187  uhgrspansubgrlem  29493  istrl  29897  ispth  29923  isspth  29924  dfpth2  29931  upgrwlkdvspth  29941  uhgrwkspthlem1  29955  uhgrwkspthlem2  29956  usgr2wlkspthlem1  29959  usgr2wlkspthlem2  29960  pthdlem1  29968  2spthd  30143  0spth  30330  3spthd  30380  trlsegvdeglem2  30425  trlsegvdeglem3  30426  ajfun  31065  fresf1o  32835  padct  32922  smatrcl  34095  esum2dlem  34391  omssubadd  34599  sitgf  34646  funen1cnv  35384  pthhashvtx  35483  satfv0fun  35726  satffunlem1  35762  satffunlem2  35763  satffun  35764  satefvfmla0  35773  satefvfmla1  35780  fperdvper  46498  ovnovollem1  47235  funressnmo  47645  dfateq12d  47725  afvres  47771  funressndmafv2rn  47822  afv2res  47838  upgrimpths  48536  fdivval  49166  idfth  49784  idsubc  49786