Theorem funeqi 6451

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

Syntax hints:   ↔ wb 205   = wceq 1541  Fun wfun 6424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908  df-br 5079  df-opab 5141  df-rel 5595  df-cnv 5596  df-co 5597  df-fun 6432

This theorem is referenced by:  funmpt  6468  funmpt2  6469  funco  6470  funresfunco  6471  fununfun  6478  funprg  6484  funtpg  6485  funtp  6487  funcnvpr  6492  funcnvtp  6493  funcnvqp  6494  funcnv0  6496  f1cnvcnv  6676  f1cof1  6677  f1coOLD  6679  opabiotafun  6843  fvn0ssdmfun  6946  funopdmsn  7016  fpropnf1  7134  funoprabg  7386  mpofun  7389  mpofunOLD  7390  ovidig  7406  funcnvuni  7765  fiun  7772  f1iun  7773  tposfun  8042  tfr1a  8209  tz7.44lem1  8220  tz7.48-2  8257  ssdomg  8757  sbthlem7  8845  sbthlem8  8846  1sdom  8987  hartogslem1  9262  r1funlim  9508  zorn2lem4  10239  axaddf  10885  axmulf  10886  fundmge2nop0  14187  funcnvs1  14606  strleun  16839  fthoppc  17620  cnfldfun  20590  cnfldfunOLD  20591  cnfldfunALT  20592  volf  24674  dfrelog  25702  usgredg3  27564  ushgredgedg  27577  ushgredgedgloop  27579  2trld  28282  0pth  28468  1pthdlem1  28478  1trld  28485  3trld  28515  ajfuni  29200  hlimf  29578  funadj  30227  funcnvadj  30234  rinvf1o  30944  bnj97  32825  bnj150  32835  bnj1384  32991  bnj1421  33001  bnj60  33021  satffunlem2lem2  33347  satfv0fvfmla0  33354  funpartfun  34224  funtransport  34312  funray  34421  funline  34423  xlimfun  43350  funcoressn  44487