Theorem funeqi 6506

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

Syntax hints:   ↔ wb 207   = wceq 1547  Fun wfun 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-br 5073  df-opab 5135  df-rel 5625  df-cnv 5626  df-co 5627  df-fun 6487

This theorem is referenced by:  funmpt  6523  funmpt2  6524  funco  6525  funresfunco  6526  fununfun  6533  funprg  6539  funtpg  6540  funtp  6542  funcnvpr  6547  funcnvtp  6548  funcnvqp  6549  funcnv0  6551  f1cnvcnv  6732  f1cof1  6733  f1oi  6805  opabiotafun  6907  fvn0ssdmfun  7015  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  8937  sbthlem7  9021  sbthlem8  9022  hartogslem1  9447  r1funlim  9681  zorn2lem4  10412  axaddf  11059  axmulf  11060  fundmge2nop0  14455  funcnvs1  14865  strleun  17118  fthoppc  17883  cnfldfun  21361  cnfldfunALT  21362  volf  25514  dfrelog  26547  precsexlem10  28226  precsexlem11  28227  usgredg3  29303  ushgredgedg  29316  ushgredgedgloop  29318  2trld  30024  0pth  30213  1pthdlem1  30223  1trld  30230  3trld  30260  ajfuni  30948  hlimf  31326  funadj  31975  funcnvadj  31982  rinvf1o  32722  isconstr  33920  bnj97  35048  bnj150  35058  bnj1384  35214  bnj1421  35224  bnj60  35244  satffunlem2lem2  35634  satfv0fvfmla0  35641  funpartfun  36171  funtransport  36259  funray  36368  funline  36370  modelaxreplem2  45423  xlimfun  46298  funcoressn  47505  upgrimpthslem1  48398  upgrimspths  48401