Theorem funeqi 6511

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

Syntax hints:   ↔ wb 206   = wceq 1541  Fun wfun 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916  df-br 5097  df-opab 5159  df-rel 5629  df-cnv 5630  df-co 5631  df-fun 6492

This theorem is referenced by:  funmpt  6528  funmpt2  6529  funco  6530  funresfunco  6531  fununfun  6538  funprg  6544  funtpg  6545  funtp  6547  funcnvpr  6552  funcnvtp  6553  funcnvqp  6554  funcnv0  6556  f1cnvcnv  6737  f1cof1  6738  f1oi  6810  opabiotafun  6912  fvn0ssdmfun  7017  funopdmsn  7093  fpropnf1  7211  funoprabg  7477  mpofun  7480  ovidig  7498  funcnvuni  7872  resf1extb  7874  fiun  7885  f1iun  7886  tposfun  8182  tfr1a  8323  tz7.44lem1  8334  tz7.48-2  8371  ssdomg  8935  sbthlem7  9019  sbthlem8  9020  hartogslem1  9445  r1funlim  9676  zorn2lem4  10407  axaddf  11054  axmulf  11055  fundmge2nop0  14423  funcnvs1  14833  strleun  17082  fthoppc  17847  cnfldfun  21321  cnfldfunALT  21322  cnfldfunOLD  21334  cnfldfunALTOLD  21335  volf  25484  dfrelog  26528  precsexlem10  28184  precsexlem11  28185  usgredg3  29238  ushgredgedg  29251  ushgredgedgloop  29253  2trld  29960  0pth  30149  1pthdlem1  30159  1trld  30166  3trld  30196  ajfuni  30883  hlimf  31261  funadj  31910  funcnvadj  31917  rinvf1o  32657  isconstr  33842  bnj97  34971  bnj150  34981  bnj1384  35137  bnj1421  35147  bnj60  35167  satffunlem2lem2  35549  satfv0fvfmla0  35556  funpartfun  36086  funtransport  36174  funray  36283  funline  36285  modelaxreplem2  45162  xlimfun  46041  funcoressn  47230  upgrimpthslem1  48095  upgrimspths  48098