Theorem funeqi 6540

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-fun 6516

This theorem is referenced by:  funmpt  6557  funmpt2  6558  funco  6559  funresfunco  6560  fununfun  6567  funprg  6573  funtpg  6574  funtp  6576  funcnvpr  6581  funcnvtp  6582  funcnvqp  6583  funcnv0  6585  f1cnvcnv  6768  f1cof1  6769  opabiotafun  6944  fvn0ssdmfun  7049  funopdmsn  7125  fpropnf1  7245  funoprabg  7513  mpofun  7516  ovidig  7534  funcnvuni  7911  resf1extb  7913  fiun  7924  f1iun  7925  tposfun  8224  tfr1a  8365  tz7.44lem1  8376  tz7.48-2  8413  ssdomg  8974  sbthlem7  9063  sbthlem8  9064  1sdomOLD  9203  hartogslem1  9502  r1funlim  9726  zorn2lem4  10459  axaddf  11105  axmulf  11106  fundmge2nop0  14474  funcnvs1  14885  strleun  17134  fthoppc  17894  cnfldfun  21285  cnfldfunALT  21286  cnfldfunOLD  21298  cnfldfunALTOLD  21299  volf  25437  dfrelog  26481  precsexlem10  28125  precsexlem11  28126  usgredg3  29150  ushgredgedg  29163  ushgredgedgloop  29165  2trld  29875  0pth  30061  1pthdlem1  30071  1trld  30078  3trld  30108  ajfuni  30795  hlimf  31173  funadj  31822  funcnvadj  31829  rinvf1o  32561  isconstr  33733  bnj97  34863  bnj150  34873  bnj1384  35029  bnj1421  35039  bnj60  35059  satffunlem2lem2  35400  satfv0fvfmla0  35407  funpartfun  35938  funtransport  36026  funray  36135  funline  36137  modelaxreplem2  44976  xlimfun  45860  funcoressn  47047  upgrimpthslem1  47911  upgrimspths  47914