Theorem funeqi 6557

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-br 5120  df-opab 5182  df-rel 5661  df-cnv 5662  df-co 5663  df-fun 6533

This theorem is referenced by:  funmpt  6574  funmpt2  6575  funco  6576  funresfunco  6577  fununfun  6584  funprg  6590  funtpg  6591  funtp  6593  funcnvpr  6598  funcnvtp  6599  funcnvqp  6600  funcnv0  6602  f1cnvcnv  6783  f1cof1  6784  opabiotafun  6959  fvn0ssdmfun  7064  funopdmsn  7140  fpropnf1  7260  funoprabg  7528  mpofun  7531  ovidig  7549  funcnvuni  7928  resf1extb  7930  fiun  7941  f1iun  7942  tposfun  8241  tfr1a  8408  tz7.44lem1  8419  tz7.48-2  8456  ssdomg  9014  sbthlem7  9103  sbthlem8  9104  1sdomOLD  9257  hartogslem1  9556  r1funlim  9780  zorn2lem4  10513  axaddf  11159  axmulf  11160  fundmge2nop0  14520  funcnvs1  14931  strleun  17176  fthoppc  17938  cnfldfun  21329  cnfldfunALT  21330  cnfldfunOLD  21342  cnfldfunALTOLD  21343  volf  25482  dfrelog  26526  precsexlem10  28170  precsexlem11  28171  usgredg3  29195  ushgredgedg  29208  ushgredgedgloop  29210  2trld  29920  0pth  30106  1pthdlem1  30116  1trld  30123  3trld  30153  ajfuni  30840  hlimf  31218  funadj  31867  funcnvadj  31874  rinvf1o  32608  isconstr  33770  bnj97  34897  bnj150  34907  bnj1384  35063  bnj1421  35073  bnj60  35093  satffunlem2lem2  35428  satfv0fvfmla0  35435  funpartfun  35961  funtransport  36049  funray  36158  funline  36160  modelaxreplem2  45004  xlimfun  45884  funcoressn  47071  upgrimpthslem1  47920  upgrimspths  47923