Theorem funeqi 6514

Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
funeqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
funeqi	⊢ (Fun 𝐴 ↔ Fun 𝐵)

Proof of Theorem funeqi

Step	Hyp	Ref	Expression
1		funeqi.1	. 2 ⊢ 𝐴 = 𝐵
2		funeq 6513	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐴 ↔ Fun 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1542  Fun wfun 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-rel 5632  df-cnv 5633  df-co 5634  df-fun 6495

This theorem is referenced by:  funmpt  6531  funmpt2  6532  funco  6533  funresfunco  6534  fununfun  6541  funprg  6547  funtpg  6548  funtp  6550  funcnvpr  6555  funcnvtp  6556  funcnvqp  6557  funcnv0  6559  f1cnvcnv  6740  f1cof1  6741  f1oi  6813  opabiotafun  6915  fvn0ssdmfun  7021  funopdmsn  7098  fpropnf1  7216  funoprabg  7482  mpofun  7485  ovidig  7503  funcnvuni  7877  resf1extb  7879  fiun  7890  f1iun  7891  tposfun  8186  tfr1a  8327  tz7.44lem1  8338  tz7.48-2  8375  ssdomg  8941  sbthlem7  9025  sbthlem8  9026  hartogslem1  9451  r1funlim  9684  zorn2lem4  10415  axaddf  11062  axmulf  11063  fundmge2nop0  14458  funcnvs1  14868  strleun  17121  fthoppc  17886  cnfldfun  21361  cnfldfunALT  21362  cnfldfunOLD  21374  cnfldfunALTOLD  21375  volf  25509  dfrelog  26545  precsexlem10  28225  precsexlem11  28226  usgredg3  29302  ushgredgedg  29315  ushgredgedgloop  29317  2trld  30024  0pth  30213  1pthdlem1  30223  1trld  30230  3trld  30260  ajfuni  30948  hlimf  31326  funadj  31975  funcnvadj  31982  rinvf1o  32721  isconstr  33899  bnj97  35027  bnj150  35037  bnj1384  35193  bnj1421  35203  bnj60  35223  satffunlem2lem2  35607  satfv0fvfmla0  35614  funpartfun  36144  funtransport  36232  funray  36341  funline  36343  modelaxreplem2  45427  xlimfun  46304  funcoressn  47505  upgrimpthslem1  48398  upgrimspths  48401