Theorem funeqi 6558

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

Syntax hints:   ↔ wb 209   = wceq 1567  Fun wfun 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-br 5114  df-opab 5178  df-rel 5669  df-cnv 5670  df-co 5671  df-fun 6539

This theorem is referenced by:  funmpt  6575  funmpt2  6576  funco  6577  funresfunco  6578  fununfun  6585  funprg  6591  funtpg  6592  funtp  6594  funcnvpr  6599  funcnvtp  6600  funcnvqp  6601  funcnv0  6603  f1cnvcnv  6786  f1cof1  6787  f1oi  6860  opabiotafun  6962  fvn0ssdmfun  7070  funopdmsn  7148  fpropnf1  7266  funoprabg  7532  mpofun  7535  ovidig  7553  funcnvuni  7929  resf1extb  7931  fiun  7940  f1iun  7941  tposfun  8238  tfr1a  8381  tz7.44lem1  8392  tz7.48-2  8429  ssdomg  8997  sbthlem7  9081  sbthlem8  9082  hartogslem1  9504  r1funlim  9738  zorn2lem4  10483  axaddf  11130  axmulf  11131  fundmge2nop0  14539  funcnvs1  14949  strleun  17217  fthoppc  17982  cnfldfun  21505  cnfldfunALT  21506  volf  25657  dfrelog  26696  precsexlem10  28375  precsexlem11  28376  usgredg3  29507  ushgredgedg  29520  ushgredgedgloop  29522  2trld  30228  0pth  30417  1pthdlem1  30427  1trld  30434  3trld  30464  ajfuni  31152  hlimf  31530  funadj  32179  funcnvadj  32186  rinvf1o  32916  isconstr  34071  bnj97  35199  bnj150  35209  bnj1384  35365  bnj1421  35375  bnj60  35395  satffunlem2lem2  35797  satfv0fvfmla0  35804  funpartfun  36334  funtransport  36422  funray  36531  funline  36533  modelaxreplem2  45580  xlimfun  46461  funcoressn  47668  upgrimpthslem1  48561  upgrimspths  48564