Theorem funeqi 6577

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

Syntax hints:   ↔ wb 205   = wceq 1533  Fun wfun 6545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3473  df-in 3954  df-ss 3964  df-br 5151  df-opab 5213  df-rel 5687  df-cnv 5688  df-co 5689  df-fun 6553

This theorem is referenced by:  funmpt  6594  funmpt2  6595  funco  6596  funresfunco  6597  fununfun  6604  funprg  6610  funtpg  6611  funtp  6613  funcnvpr  6618  funcnvtp  6619  funcnvqp  6620  funcnv0  6622  f1cnvcnv  6806  f1cof1  6807  f1coOLD  6809  opabiotafun  6982  fvn0ssdmfun  7087  funopdmsn  7163  fpropnf1  7281  funoprabg  7545  mpofun  7548  mpofunOLD  7549  ovidig  7567  funcnvuni  7943  fiun  7950  f1iun  7951  tposfun  8252  tfr1a  8419  tz7.44lem1  8430  tz7.48-2  8467  ssdomg  9025  sbthlem7  9118  sbthlem8  9119  1sdomOLD  9278  hartogslem1  9571  r1funlim  9795  zorn2lem4  10528  axaddf  11174  axmulf  11175  fundmge2nop0  14491  funcnvs1  14901  strleun  17131  fthoppc  17917  cnfldfun  21298  cnfldfunALT  21299  cnfldfunOLD  21311  cnfldfunALTOLD  21312  cnfldfunALTOLDOLD  21313  volf  25476  dfrelog  26517  precsexlem10  28132  precsexlem11  28133  usgredg3  29047  ushgredgedg  29060  ushgredgedgloop  29062  2trld  29767  0pth  29953  1pthdlem1  29963  1trld  29970  3trld  30000  ajfuni  30687  hlimf  31065  funadj  31714  funcnvadj  31721  rinvf1o  32433  bnj97  34502  bnj150  34512  bnj1384  34668  bnj1421  34678  bnj60  34698  satffunlem2lem2  35021  satfv0fvfmla0  35028  funpartfun  35544  funtransport  35632  funray  35741  funline  35743  xlimfun  45245  funcoressn  46426