Theorem funeqi 6527

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

Syntax hints:   ↔ wb 205   = wceq 1541  Fun wfun 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-br 5111  df-opab 5173  df-rel 5645  df-cnv 5646  df-co 5647  df-fun 6503

This theorem is referenced by:  funmpt  6544  funmpt2  6545  funco  6546  funresfunco  6547  fununfun  6554  funprg  6560  funtpg  6561  funtp  6563  funcnvpr  6568  funcnvtp  6569  funcnvqp  6570  funcnv0  6572  f1cnvcnv  6753  f1cof1  6754  f1coOLD  6756  opabiotafun  6927  fvn0ssdmfun  7030  funopdmsn  7101  fpropnf1  7219  funoprabg  7482  mpofun  7485  mpofunOLD  7486  ovidig  7502  funcnvuni  7873  fiun  7880  f1iun  7881  tposfun  8178  tfr1a  8345  tz7.44lem1  8356  tz7.48-2  8393  ssdomg  8947  sbthlem7  9040  sbthlem8  9041  1sdomOLD  9200  hartogslem1  9487  r1funlim  9711  zorn2lem4  10444  axaddf  11090  axmulf  11091  fundmge2nop0  14403  funcnvs1  14813  strleun  17040  fthoppc  17824  cnfldfun  20845  cnfldfunALT  20846  cnfldfunALTOLD  20847  volf  24930  dfrelog  25958  usgredg3  28227  ushgredgedg  28240  ushgredgedgloop  28242  2trld  28946  0pth  29132  1pthdlem1  29142  1trld  29149  3trld  29179  ajfuni  29864  hlimf  30242  funadj  30891  funcnvadj  30898  rinvf1o  31611  bnj97  33567  bnj150  33577  bnj1384  33733  bnj1421  33743  bnj60  33763  satffunlem2lem2  34087  satfv0fvfmla0  34094  funpartfun  34604  funtransport  34692  funray  34801  funline  34803  xlimfun  44216  funcoressn  45396