Theorem funeqi 6554

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

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

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-rel 5662  df-cnv 5663  df-co 5664  df-fun 6535

This theorem is used by:  funmpt  6572  funmpt2  6573  funco  6574  funresfunco  6575  fununfun  6582  funprg  6588  funtpg  6589  funtp  6591  funcnvpr  6596  funcnvtp  6597  funcnvqp  6598  funcnv0  6600  f1cnvcnv  6783  f1cof1  6784  f1oi  6857  opabiotafun  6959  fvn0ssdmfun  7068  funopdmsn  7148  fpropnf1  7265  funoprabg  7535  mpofun  7538  ovidig  7556  funcnvuni  7930  resf1extb  7932  fiun  7941  f1iun  7942  tposfun  8241  tfr1a  8384  tz7.44lem1  8395  tz7.48-2  8434  ssdomg  9009  sbthlem7  9094  sbthlem8  9095  hartogslem1  9517  r1funlim  9751  zorn2lem4  10504  axaddf  11157  axmulf  11158  fundmge2nop0  14570  funcnvs1  14986  strleun  17252  fthoppc  18017  mgmn0plusgf  18744  degenmgm2nfun  19055  cnfldfun  21602  cnfldfunALT  21603  volf  25760  dfrelog  26805  precsexlem10  28484  precsexlem11  28485  usgredg3  29679  ushgredgedg  29692  ushgredgedgloop  29694  2trld  30409  0pth  30598  1pthdlem1  30608  1trld  30615  3trld  30655  ajfuni  31343  hlimf  31721  funadj  32370  funcnvadj  32377  rinvf1o  33106  isconstr  34249  bnj97  35378  bnj150  35388  bnj1384  35544  bnj1421  35554  bnj60  35574  satffunlem2lem2  35988  satfv0fvfmla0  35995  funpartfun  36525  funtransport  36614  funray  36723  funline  36725  modelaxreplem2  45805  xlimfun  46686  funcoressn  47933  upgrimpthslem1  48826  upgrimspths  48829