Theorem funeqi 6521

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 6520	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐴 ↔ Fun 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1540  Fun wfun 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-rel 5638  df-cnv 5639  df-co 5640  df-fun 6501

This theorem is referenced by:  funmpt  6538  funmpt2  6539  funco  6540  funresfunco  6541  fununfun  6548  funprg  6554  funtpg  6555  funtp  6557  funcnvpr  6562  funcnvtp  6563  funcnvqp  6564  funcnv0  6566  f1cnvcnv  6747  f1cof1  6748  opabiotafun  6923  fvn0ssdmfun  7028  funopdmsn  7104  fpropnf1  7224  funoprabg  7490  mpofun  7493  ovidig  7511  funcnvuni  7888  resf1extb  7890  fiun  7901  f1iun  7902  tposfun  8198  tfr1a  8339  tz7.44lem1  8350  tz7.48-2  8387  ssdomg  8948  sbthlem7  9034  sbthlem8  9035  1sdomOLD  9172  hartogslem1  9471  r1funlim  9695  zorn2lem4  10428  axaddf  11074  axmulf  11075  fundmge2nop0  14443  funcnvs1  14854  strleun  17103  fthoppc  17867  cnfldfun  21310  cnfldfunALT  21311  cnfldfunOLD  21323  cnfldfunALTOLD  21324  volf  25463  dfrelog  26507  precsexlem10  28158  precsexlem11  28159  usgredg3  29196  ushgredgedg  29209  ushgredgedgloop  29211  2trld  29918  0pth  30104  1pthdlem1  30114  1trld  30121  3trld  30151  ajfuni  30838  hlimf  31216  funadj  31865  funcnvadj  31872  rinvf1o  32604  isconstr  33719  bnj97  34849  bnj150  34859  bnj1384  35015  bnj1421  35025  bnj60  35045  satffunlem2lem2  35386  satfv0fvfmla0  35393  funpartfun  35924  funtransport  36012  funray  36121  funline  36123  modelaxreplem2  44962  xlimfun  45846  funcoressn  47036  upgrimpthslem1  47900  upgrimspths  47903