Theorem funeqi 6246

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

Syntax hints:   ↔ wb 207   = wceq 1522  Fun wfun 6219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-in 3866  df-ss 3874  df-br 4963  df-opab 5025  df-rel 5450  df-cnv 5451  df-co 5452  df-fun 6227

This theorem is referenced by:  funmpt  6263  funmpt2  6264  funco  6265  funresfunco  6266  fununfun  6272  funprg  6278  funtpg  6279  funtp  6281  funcnvpr  6286  funcnvtp  6287  funcnvqp  6288  funcnv0  6290  f1cnvcnv  6452  f1co  6453  opabiotafun  6611  fvn0ssdmfun  6707  funopdmsn  6775  fpropnf1  6890  funoprabg  7129  mpofun  7132  ovidig  7148  funcnvuni  7492  fiun  7500  f1iun  7501  tposfun  7759  tfr1a  7882  tz7.44lem1  7893  tz7.48-2  7929  ssdomg  8403  sbthlem7  8480  sbthlem8  8481  1sdom  8567  hartogslem1  8852  r1funlim  9041  zorn2lem4  9767  axaddf  10413  axmulf  10414  fundmge2nop0  13696  funcnvs1  14110  strleun  16420  fthoppc  17022  cnfldfun  20239  cnfldfunALT  20240  volf  23813  dfrelog  24830  usgredg3  26681  ushgredgedg  26694  ushgredgedgloop  26696  2trld  27404  0pth  27591  1pthdlem1  27601  1trld  27608  3trld  27638  ajfuni  28327  hlimf  28705  funadj  29354  funcnvadj  29361  rinvf1o  30065  bnj97  31754  bnj150  31764  bnj1384  31918  bnj1421  31928  bnj60  31948  satffunlem2lem2  32261  satfv0fvfmla0  32268  funpartfun  33013  funtransport  33101  funray  33210  funline  33212  xlimfun  41678  funcoressn  42793