Theorem funeqi 6379

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

Syntax hints:   ↔ wb 209   = wceq 1543  Fun wfun 6352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-br 5040  df-opab 5102  df-rel 5543  df-cnv 5544  df-co 5545  df-fun 6360

This theorem is referenced by:  funmpt  6396  funmpt2  6397  funco  6398  funresfunco  6399  fununfun  6406  funprg  6412  funtpg  6413  funtp  6415  funcnvpr  6420  funcnvtp  6421  funcnvqp  6422  funcnv0  6424  f1cnvcnv  6603  f1cof1  6604  f1coOLD  6606  opabiotafun  6770  fvn0ssdmfun  6873  funopdmsn  6943  fpropnf1  7057  funoprabg  7309  mpofun  7312  mpofunOLD  7313  ovidig  7329  funcnvuni  7687  fiun  7694  f1iun  7695  tposfun  7962  tfr1a  8108  tz7.44lem1  8119  tz7.48-2  8156  ssdomg  8652  sbthlem7  8740  sbthlem8  8741  1sdom  8857  hartogslem1  9136  r1funlim  9347  zorn2lem4  10078  axaddf  10724  axmulf  10725  fundmge2nop0  14023  funcnvs1  14442  strleun  16775  fthoppc  17384  cnfldfun  20329  cnfldfunALT  20330  volf  24380  dfrelog  25408  usgredg3  27258  ushgredgedg  27271  ushgredgedgloop  27273  2trld  27976  0pth  28162  1pthdlem1  28172  1trld  28179  3trld  28209  ajfuni  28894  hlimf  29272  funadj  29921  funcnvadj  29928  rinvf1o  30638  bnj97  32513  bnj150  32523  bnj1384  32679  bnj1421  32689  bnj60  32709  satffunlem2lem2  33035  satfv0fvfmla0  33042  funpartfun  33931  funtransport  34019  funray  34128  funline  34130  bj-isrvec  35148  xlimfun  43014  funcoressn  44151