Theorem funeqi 6542

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

Syntax hints:   ↔ wb 208   = wceq 1560  Fun wfun 6515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-br 5101  df-opab 5163  df-rel 5654  df-cnv 5655  df-co 5656  df-fun 6523

This theorem is referenced by:  funmpt  6559  funmpt2  6560  funco  6561  funresfunco  6562  fununfun  6569  funprg  6575  funtpg  6576  funtp  6578  funcnvpr  6583  funcnvtp  6584  funcnvqp  6585  funcnv0  6587  f1cnvcnv  6771  f1cof1  6772  f1oi  6845  opabiotafun  6947  fvn0ssdmfun  7055  funopdmsn  7133  fpropnf1  7251  funoprabg  7517  mpofun  7520  ovidig  7538  funcnvuni  7913  resf1extb  7915  fiun  7924  f1iun  7925  tposfun  8222  tfr1a  8365  tz7.44lem1  8376  tz7.48-2  8413  ssdomg  8981  sbthlem7  9065  sbthlem8  9066  hartogslem1  9490  r1funlim  9724  zorn2lem4  10456  axaddf  11103  axmulf  11104  fundmge2nop0  14515  funcnvs1  14925  strleun  17193  fthoppc  17958  cnfldfun  21438  cnfldfunALT  21439  volf  25591  dfrelog  26630  precsexlem10  28309  precsexlem11  28310  usgredg3  29417  ushgredgedg  29430  ushgredgedgloop  29432  2trld  30138  0pth  30327  1pthdlem1  30337  1trld  30344  3trld  30374  ajfuni  31062  hlimf  31440  funadj  32089  funcnvadj  32096  rinvf1o  32832  isconstr  34033  bnj97  35161  bnj150  35171  bnj1384  35327  bnj1421  35337  bnj60  35357  satffunlem2lem2  35756  satfv0fvfmla0  35763  funpartfun  36293  funtransport  36381  funray  36490  funline  36492  modelaxreplem2  45555  xlimfun  46429  funcoressn  47636  upgrimpthslem1  48529  upgrimspths  48532