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 𝐵)

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5109  df-opab 5174  df-rel 5665  df-cnv 5666  df-co 5667  df-fun 6568

This theorem is used by:  funmpt  6606  funmpt2  6607  funco  6608  funresfunco  6609  fununfunOLD  6617  funprg  6624  funtpg  6625  funtp  6627  funcnvpr  6632  funcnvtp  6633  funcnvqp  6634  funcnv0  6636  f1cnvcnv  6819  f1cof1  6820  f1oi  6894  opabiotafun  6996  fvn0ssdmfun  7106  funopdmsn  7186  fpropnf1  7302  funoprabg  7572  mpofun  7575  ovidig  7594  funmpt3  7719  funcnvuni  7978  resf1extb  7980  fiun  7989  f1iun  7990  tposfun  8297  tfr1a  8440  tz7.44lem1  8451  tz7.48-2  8490  ssdomg  9065  sbthlem7  9150  sbthlem8  9151  hartogslem1  9573  r1funlimOLD  9807  r1fun  9808  zorn2lem4  10616  axaddf  11269  axmulf  11270  fundmge2nop0  14688  funcnvs1  15106  strleun  17379  fthoppc  18150  mgmn0plusgf  18877  degenmgm2nfun  19189  cnfldfun  21744  cnfldfunALT  21745  volf  25905  dfrelog  26950  precsexlem10  28659  precsexlem11  28660  usgredg3  29854  ushgredgedg  29867  ushgredgedgloop  29869  2trld  30584  0pth  30773  1pthdlem1  30783  1trld  30790  3trld  30830  ajfuni  31518  hlimf  31896  funadj  32545  funcnvadj  32552  rinvf1o  33322  isconstr  34479  bnj97  35607  bnj150  35617  bnj1384  35773  bnj1421  35783  bnj60  35803  fwfffun  35828  srepdflem1  36126  srepdflem2  36127  satffunlem2lem2  36379  satfv0fvfmla0  36386  funpartfun  36922  funtransport  37011  funray  37120  funline  37122  modelaxreplem2  46233  xlimfun  47138  funcoressn  48385  upgrimpthslem1  49278  upgrimspths  49281