Theorem funeqi 6588

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

Syntax hints:   ↔ wb 206   = wceq 1536  Fun wfun 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-br 5148  df-opab 5210  df-rel 5695  df-cnv 5696  df-co 5697  df-fun 6564

This theorem is referenced by:  funmpt  6605  funmpt2  6606  funco  6607  funresfunco  6608  fununfun  6615  funprg  6621  funtpg  6622  funtp  6624  funcnvpr  6629  funcnvtp  6630  funcnvqp  6631  funcnv0  6633  f1cnvcnv  6813  f1cof1  6814  opabiotafun  6988  fvn0ssdmfun  7093  funopdmsn  7169  fpropnf1  7286  funoprabg  7553  mpofun  7556  ovidig  7574  funcnvuni  7954  fiun  7965  f1iun  7966  tposfun  8265  tfr1a  8432  tz7.44lem1  8443  tz7.48-2  8480  ssdomg  9038  sbthlem7  9127  sbthlem8  9128  1sdomOLD  9282  hartogslem1  9579  r1funlim  9803  zorn2lem4  10536  axaddf  11182  axmulf  11183  fundmge2nop0  14537  funcnvs1  14947  strleun  17190  fthoppc  17976  cnfldfun  21395  cnfldfunALT  21396  cnfldfunOLD  21408  cnfldfunALTOLD  21409  cnfldfunALTOLDOLD  21410  volf  25577  dfrelog  26621  precsexlem10  28254  precsexlem11  28255  usgredg3  29247  ushgredgedg  29260  ushgredgedgloop  29262  2trld  29967  0pth  30153  1pthdlem1  30163  1trld  30170  3trld  30200  ajfuni  30887  hlimf  31265  funadj  31914  funcnvadj  31921  rinvf1o  32646  bnj97  34858  bnj150  34868  bnj1384  35024  bnj1421  35034  bnj60  35054  satffunlem2lem2  35390  satfv0fvfmla0  35397  funpartfun  35924  funtransport  36012  funray  36121  funline  36123  modelaxreplem2  44943  xlimfun  45810  funcoressn  46991