Theorem funeqi 6539

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

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

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 3933  df-br 5110  df-opab 5172  df-rel 5647  df-cnv 5648  df-co 5649  df-fun 6515

This theorem is referenced by:  funmpt  6556  funmpt2  6557  funco  6558  funresfunco  6559  fununfun  6566  funprg  6572  funtpg  6573  funtp  6575  funcnvpr  6580  funcnvtp  6581  funcnvqp  6582  funcnv0  6584  f1cnvcnv  6767  f1cof1  6768  opabiotafun  6943  fvn0ssdmfun  7048  funopdmsn  7124  fpropnf1  7244  funoprabg  7512  mpofun  7515  ovidig  7533  funcnvuni  7910  resf1extb  7912  fiun  7923  f1iun  7924  tposfun  8223  tfr1a  8364  tz7.44lem1  8375  tz7.48-2  8412  ssdomg  8973  sbthlem7  9062  sbthlem8  9063  1sdomOLD  9202  hartogslem1  9501  r1funlim  9725  zorn2lem4  10458  axaddf  11104  axmulf  11105  fundmge2nop0  14473  funcnvs1  14884  strleun  17133  fthoppc  17893  cnfldfun  21284  cnfldfunALT  21285  cnfldfunOLD  21297  cnfldfunALTOLD  21298  volf  25436  dfrelog  26480  precsexlem10  28124  precsexlem11  28125  usgredg3  29149  ushgredgedg  29162  ushgredgedgloop  29164  2trld  29874  0pth  30060  1pthdlem1  30070  1trld  30077  3trld  30107  ajfuni  30794  hlimf  31172  funadj  31821  funcnvadj  31828  rinvf1o  32560  isconstr  33732  bnj97  34862  bnj150  34872  bnj1384  35028  bnj1421  35038  bnj60  35058  satffunlem2lem2  35393  satfv0fvfmla0  35400  funpartfun  35926  funtransport  36014  funray  36123  funline  36125  modelaxreplem2  44962  xlimfun  45846  funcoressn  47033  upgrimpthslem1  47897  upgrimspths  47900