Theorem funeqi 6503

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

Syntax hints:   ↔ wb 206   = wceq 1540  Fun wfun 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3920  df-br 5093  df-opab 5155  df-rel 5626  df-cnv 5627  df-co 5628  df-fun 6484

This theorem is referenced by:  funmpt  6520  funmpt2  6521  funco  6522  funresfunco  6523  fununfun  6530  funprg  6536  funtpg  6537  funtp  6539  funcnvpr  6544  funcnvtp  6545  funcnvqp  6546  funcnv0  6548  f1cnvcnv  6729  f1cof1  6730  opabiotafun  6903  fvn0ssdmfun  7008  funopdmsn  7084  fpropnf1  7204  funoprabg  7470  mpofun  7473  ovidig  7491  funcnvuni  7865  resf1extb  7867  fiun  7878  f1iun  7879  tposfun  8175  tfr1a  8316  tz7.44lem1  8327  tz7.48-2  8364  ssdomg  8925  sbthlem7  9010  sbthlem8  9011  hartogslem1  9434  r1funlim  9662  zorn2lem4  10393  axaddf  11039  axmulf  11040  fundmge2nop0  14409  funcnvs1  14819  strleun  17068  fthoppc  17832  cnfldfun  21275  cnfldfunALT  21276  cnfldfunOLD  21288  cnfldfunALTOLD  21289  volf  25428  dfrelog  26472  precsexlem10  28123  precsexlem11  28124  usgredg3  29161  ushgredgedg  29174  ushgredgedgloop  29176  2trld  29883  0pth  30069  1pthdlem1  30079  1trld  30086  3trld  30116  ajfuni  30803  hlimf  31181  funadj  31830  funcnvadj  31837  rinvf1o  32574  isconstr  33709  bnj97  34839  bnj150  34849  bnj1384  35005  bnj1421  35015  bnj60  35035  satffunlem2lem2  35389  satfv0fvfmla0  35396  funpartfun  35927  funtransport  36015  funray  36124  funline  36126  modelaxreplem2  44963  xlimfun  45846  funcoressn  47036  upgrimpthslem1  47901  upgrimspths  47904