Theorem funeqi 6557

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

Syntax hints:   ↔ wb 209   = wceq 1570  Fun wfun 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5110  df-opab 5174  df-rel 5668  df-cnv 5669  df-co 5670  df-fun 6538

This theorem is referenced by:  funmpt  6574  funmpt2  6575  funco  6576  funresfunco  6577  fununfun  6584  funprg  6590  funtpg  6591  funtp  6593  funcnvpr  6598  funcnvtp  6599  funcnvqp  6600  funcnv0  6602  f1cnvcnv  6785  f1cof1  6786  f1oi  6859  opabiotafun  6961  fvn0ssdmfun  7069  funopdmsn  7147  fpropnf1  7265  funoprabg  7531  mpofun  7534  ovidig  7552  funcnvuni  7925  resf1extb  7927  fiun  7936  f1iun  7937  tposfun  8234  tfr1a  8377  tz7.44lem1  8388  tz7.48-2  8425  ssdomg  8993  sbthlem7  9077  sbthlem8  9078  hartogslem1  9500  r1funlim  9734  zorn2lem4  10478  axaddf  11125  axmulf  11126  fundmge2nop0  14535  funcnvs1  14945  strleun  17212  fthoppc  17977  cnfldfun  21536  cnfldfunALT  21537  volf  25688  dfrelog  26730  precsexlem10  28409  precsexlem11  28410  usgredg3  29566  ushgredgedg  29579  ushgredgedgloop  29581  2trld  30287  0pth  30476  1pthdlem1  30486  1trld  30493  3trld  30523  ajfuni  31211  hlimf  31589  funadj  32238  funcnvadj  32245  rinvf1o  32975  isconstr  34126  bnj97  35254  bnj150  35264  bnj1384  35420  bnj1421  35430  bnj60  35450  satffunlem2lem2  35898  satfv0fvfmla0  35905  funpartfun  36435  funtransport  36523  funray  36632  funline  36634  modelaxreplem2  45708  xlimfun  46589  funcoressn  47799  upgrimpthslem1  48692  upgrimspths  48695