Theorem funeqi 6570

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

Syntax hints:   ↔ wb 205   = wceq 1539  Fun wfun 6538

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-rel 5684  df-cnv 5685  df-co 5686  df-fun 6546

This theorem is referenced by:  funmpt  6587  funmpt2  6588  funco  6589  funresfunco  6590  fununfun  6597  funprg  6603  funtpg  6604  funtp  6606  funcnvpr  6611  funcnvtp  6612  funcnvqp  6613  funcnv0  6615  f1cnvcnv  6798  f1cof1  6799  f1coOLD  6801  opabiotafun  6973  fvn0ssdmfun  7077  funopdmsn  7151  fpropnf1  7270  funoprabg  7533  mpofun  7536  mpofunOLD  7537  ovidig  7554  funcnvuni  7926  fiun  7933  f1iun  7934  tposfun  8231  tfr1a  8398  tz7.44lem1  8409  tz7.48-2  8446  ssdomg  9000  sbthlem7  9093  sbthlem8  9094  1sdomOLD  9253  hartogslem1  9541  r1funlim  9765  zorn2lem4  10498  axaddf  11144  axmulf  11145  fundmge2nop0  14459  funcnvs1  14869  strleun  17096  fthoppc  17880  cnfldfun  21158  cnfldfunALT  21159  cnfldfunALTOLD  21160  volf  25280  dfrelog  26308  precsexlem10  27899  precsexlem11  27900  usgredg3  28738  ushgredgedg  28751  ushgredgedgloop  28753  2trld  29457  0pth  29643  1pthdlem1  29653  1trld  29660  3trld  29690  ajfuni  30377  hlimf  30755  funadj  31404  funcnvadj  31411  rinvf1o  32119  bnj97  34173  bnj150  34183  bnj1384  34339  bnj1421  34349  bnj60  34369  satffunlem2lem2  34693  satfv0fvfmla0  34700  funpartfun  35217  funtransport  35305  funray  35414  funline  35416  gg-cnfldfun  35485  gg-cnfldfunALT  35486  xlimfun  44871  funcoressn  46052