Theorem funeqi 6502

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

Syntax hints:   ↔ wb 206   = wceq 1541  Fun wfun 6475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-br 5090  df-opab 5152  df-rel 5621  df-cnv 5622  df-co 5623  df-fun 6483

This theorem is referenced by:  funmpt  6519  funmpt2  6520  funco  6521  funresfunco  6522  fununfun  6529  funprg  6535  funtpg  6536  funtp  6538  funcnvpr  6543  funcnvtp  6544  funcnvqp  6545  funcnv0  6547  f1cnvcnv  6728  f1cof1  6729  opabiotafun  6902  fvn0ssdmfun  7007  funopdmsn  7083  fpropnf1  7201  funoprabg  7467  mpofun  7470  ovidig  7488  funcnvuni  7862  resf1extb  7864  fiun  7875  f1iun  7876  tposfun  8172  tfr1a  8313  tz7.44lem1  8324  tz7.48-2  8361  ssdomg  8922  sbthlem7  9006  sbthlem8  9007  hartogslem1  9428  r1funlim  9659  zorn2lem4  10390  axaddf  11036  axmulf  11037  fundmge2nop0  14409  funcnvs1  14819  strleun  17068  fthoppc  17832  cnfldfun  21305  cnfldfunALT  21306  cnfldfunOLD  21318  cnfldfunALTOLD  21319  volf  25457  dfrelog  26501  precsexlem10  28154  precsexlem11  28155  usgredg3  29194  ushgredgedg  29207  ushgredgedgloop  29209  2trld  29916  0pth  30105  1pthdlem1  30115  1trld  30122  3trld  30152  ajfuni  30839  hlimf  31217  funadj  31866  funcnvadj  31873  rinvf1o  32612  isconstr  33749  bnj97  34878  bnj150  34888  bnj1384  35044  bnj1421  35054  bnj60  35074  satffunlem2lem2  35450  satfv0fvfmla0  35457  funpartfun  35987  funtransport  36075  funray  36184  funline  36186  modelaxreplem2  45082  xlimfun  45963  funcoressn  47152  upgrimpthslem1  48017  upgrimspths  48020