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 1542  Fun wfun 6494

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 3920  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-fun 6502

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  f1oi  6820  opabiotafun  6922  fvn0ssdmfun  7028  funopdmsn  7105  fpropnf1  7223  funoprabg  7489  mpofun  7492  ovidig  7510  funcnvuni  7884  resf1extb  7886  fiun  7897  f1iun  7898  tposfun  8194  tfr1a  8335  tz7.44lem1  8346  tz7.48-2  8383  ssdomg  8949  sbthlem7  9033  sbthlem8  9034  hartogslem1  9459  r1funlim  9690  zorn2lem4  10421  axaddf  11068  axmulf  11069  fundmge2nop0  14437  funcnvs1  14847  strleun  17096  fthoppc  17861  cnfldfun  21335  cnfldfunALT  21336  cnfldfunOLD  21348  cnfldfunALTOLD  21349  volf  25498  dfrelog  26542  precsexlem10  28224  precsexlem11  28225  usgredg3  29301  ushgredgedg  29314  ushgredgedgloop  29316  2trld  30023  0pth  30212  1pthdlem1  30222  1trld  30229  3trld  30259  ajfuni  30947  hlimf  31325  funadj  31974  funcnvadj  31981  rinvf1o  32720  isconstr  33914  bnj97  35042  bnj150  35052  bnj1384  35208  bnj1421  35218  bnj60  35238  satffunlem2lem2  35622  satfv0fvfmla0  35629  funpartfun  36159  funtransport  36247  funray  36356  funline  36358  modelaxreplem2  45335  xlimfun  46213  funcoressn  47402  upgrimpthslem1  48267  upgrimspths  48270