Theorem funeqi 6561

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  Fun wfun 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-br 5112  df-opab 5176  df-rel 5670  df-cnv 5671  df-co 5672  df-fun 6542

This theorem is used by:  funmpt  6578  funmpt2  6579  funco  6580  funresfunco  6581  fununfun  6588  funprg  6594  funtpg  6595  funtp  6597  funcnvpr  6602  funcnvtp  6603  funcnvqp  6604  funcnv0  6606  f1cnvcnv  6789  f1cof1  6790  f1oi  6863  opabiotafun  6965  fvn0ssdmfun  7073  funopdmsn  7153  fpropnf1  7270  funoprabg  7540  mpofun  7543  ovidig  7561  funcnvuni  7935  resf1extb  7937  fiun  7946  f1iun  7947  tposfun  8244  tfr1a  8387  tz7.44lem1  8398  tz7.48-2  8435  ssdomg  9003  sbthlem7  9088  sbthlem8  9089  hartogslem1  9511  r1funlim  9745  zorn2lem4  10498  axaddf  11147  axmulf  11148  fundmge2nop0  14559  funcnvs1  14975  strleun  17241  fthoppc  18006  mgmn0plusgf  18733  degenmgm2nfun  19041  cnfldfun  21588  cnfldfunALT  21589  volf  25741  dfrelog  26783  precsexlem10  28462  precsexlem11  28463  usgredg3  29626  ushgredgedg  29639  ushgredgedgloop  29641  2trld  30356  0pth  30545  1pthdlem1  30555  1trld  30562  3trld  30596  ajfuni  31284  hlimf  31662  funadj  32311  funcnvadj  32318  rinvf1o  33048  isconstr  34192  bnj97  35321  bnj150  35331  bnj1384  35487  bnj1421  35497  bnj60  35517  satffunlem2lem2  35937  satfv0fvfmla0  35944  funpartfun  36474  funtransport  36562  funray  36671  funline  36673  modelaxreplem2  45748  xlimfun  46629  funcoressn  47839  upgrimpthslem1  48732  upgrimspths  48735