Theorem funeqi 6560

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-fun 6540

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  7074  funopdmsn  7154  fpropnf1  7271  funoprabg  7541  mpofun  7544  ovidig  7562  funmpt3  7687  funcnvuni  7944  resf1extb  7946  fiun  7955  f1iun  7956  tposfun  8259  tfr1a  8402  tz7.44lem1  8413  tz7.48-2  8452  ssdomg  9027  sbthlem7  9112  sbthlem8  9113  hartogslem1  9536  r1funlimOLD  9770  r1fun  9771  zorn2lem4  10577  axaddf  11230  axmulf  11231  fundmge2nop0  14647  funcnvs1  15063  strleun  17335  fthoppc  18100  mgmn0plusgf  18827  degenmgm2nfun  19139  cnfldfun  21692  cnfldfunALT  21693  volf  25850  dfrelog  26893  precsexlem10  28602  precsexlem11  28603  usgredg3  29797  ushgredgedg  29810  ushgredgedgloop  29812  2trld  30527  0pth  30716  1pthdlem1  30726  1trld  30733  3trld  30773  ajfuni  31461  hlimf  31839  funadj  32488  funcnvadj  32495  rinvf1o  33224  isconstr  34368  bnj97  35496  bnj150  35506  bnj1384  35662  bnj1421  35672  bnj60  35692  satffunlem2lem2  36171  satfv0fvfmla0  36178  funpartfun  36707  funtransport  36796  funray  36905  funline  36907  modelaxreplem2  45968  xlimfun  46864  funcoressn  48111  upgrimpthslem1  49004  upgrimspths  49007