Theorem funeqi 6537

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-fun 6513

This theorem is referenced by:  funmpt  6554  funmpt2  6555  funco  6556  funresfunco  6557  fununfun  6564  funprg  6570  funtpg  6571  funtp  6573  funcnvpr  6578  funcnvtp  6579  funcnvqp  6580  funcnv0  6582  f1cnvcnv  6765  f1cof1  6766  opabiotafun  6941  fvn0ssdmfun  7046  funopdmsn  7122  fpropnf1  7242  funoprabg  7510  mpofun  7513  ovidig  7531  funcnvuni  7908  resf1extb  7910  fiun  7921  f1iun  7922  tposfun  8221  tfr1a  8362  tz7.44lem1  8373  tz7.48-2  8410  ssdomg  8971  sbthlem7  9057  sbthlem8  9058  1sdomOLD  9196  hartogslem1  9495  r1funlim  9719  zorn2lem4  10452  axaddf  11098  axmulf  11099  fundmge2nop0  14467  funcnvs1  14878  strleun  17127  fthoppc  17887  cnfldfun  21278  cnfldfunALT  21279  cnfldfunOLD  21291  cnfldfunALTOLD  21292  volf  25430  dfrelog  26474  precsexlem10  28118  precsexlem11  28119  usgredg3  29143  ushgredgedg  29156  ushgredgedgloop  29158  2trld  29868  0pth  30054  1pthdlem1  30064  1trld  30071  3trld  30101  ajfuni  30788  hlimf  31166  funadj  31815  funcnvadj  31822  rinvf1o  32554  isconstr  33726  bnj97  34856  bnj150  34866  bnj1384  35022  bnj1421  35032  bnj60  35052  satffunlem2lem2  35393  satfv0fvfmla0  35400  funpartfun  35931  funtransport  36019  funray  36128  funline  36130  modelaxreplem2  44969  xlimfun  45853  funcoressn  47043  upgrimpthslem1  47907  upgrimspths  47910