Theorem funeqi 6599

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

Syntax hints:   ↔ wb 206   = wceq 1537  Fun wfun 6567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-rel 5707  df-cnv 5708  df-co 5709  df-fun 6575

This theorem is referenced by:  funmpt  6616  funmpt2  6617  funco  6618  funresfunco  6619  fununfun  6626  funprg  6632  funtpg  6633  funtp  6635  funcnvpr  6640  funcnvtp  6641  funcnvqp  6642  funcnv0  6644  f1cnvcnv  6826  f1cof1  6827  f1coOLD  6829  opabiotafun  7002  fvn0ssdmfun  7108  funopdmsn  7184  fpropnf1  7304  funoprabg  7571  mpofun  7574  ovidig  7592  funcnvuni  7972  fiun  7983  f1iun  7984  tposfun  8283  tfr1a  8450  tz7.44lem1  8461  tz7.48-2  8498  ssdomg  9060  sbthlem7  9155  sbthlem8  9156  1sdomOLD  9312  hartogslem1  9611  r1funlim  9835  zorn2lem4  10568  axaddf  11214  axmulf  11215  fundmge2nop0  14551  funcnvs1  14961  strleun  17204  fthoppc  17990  cnfldfun  21401  cnfldfunALT  21402  cnfldfunOLD  21414  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  volf  25583  dfrelog  26625  precsexlem10  28258  precsexlem11  28259  usgredg3  29251  ushgredgedg  29264  ushgredgedgloop  29266  2trld  29971  0pth  30157  1pthdlem1  30167  1trld  30174  3trld  30204  ajfuni  30891  hlimf  31269  funadj  31918  funcnvadj  31925  rinvf1o  32649  bnj97  34842  bnj150  34852  bnj1384  35008  bnj1421  35018  bnj60  35038  satffunlem2lem2  35374  satfv0fvfmla0  35381  funpartfun  35907  funtransport  35995  funray  36104  funline  36106  xlimfun  45776  funcoressn  46957