Theorem funeqi 6519

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

Syntax hints:   ↔ wb 206   = wceq 1542  Fun wfun 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-fun 6500

This theorem is referenced by:  funmpt  6536  funmpt2  6537  funco  6538  funresfunco  6539  fununfun  6546  funprg  6552  funtpg  6553  funtp  6555  funcnvpr  6560  funcnvtp  6561  funcnvqp  6562  funcnv0  6564  f1cnvcnv  6745  f1cof1  6746  f1oi  6818  opabiotafun  6920  fvn0ssdmfun  7026  funopdmsn  7104  fpropnf1  7222  funoprabg  7488  mpofun  7491  ovidig  7509  funcnvuni  7883  resf1extb  7885  fiun  7896  f1iun  7897  tposfun  8192  tfr1a  8333  tz7.44lem1  8344  tz7.48-2  8381  ssdomg  8947  sbthlem7  9031  sbthlem8  9032  hartogslem1  9457  r1funlim  9690  zorn2lem4  10421  axaddf  11068  axmulf  11069  fundmge2nop0  14464  funcnvs1  14874  strleun  17127  fthoppc  17892  cnfldfun  21366  cnfldfunALT  21367  volf  25496  dfrelog  26529  precsexlem10  28208  precsexlem11  28209  usgredg3  29285  ushgredgedg  29298  ushgredgedgloop  29300  2trld  30006  0pth  30195  1pthdlem1  30205  1trld  30212  3trld  30242  ajfuni  30930  hlimf  31308  funadj  31957  funcnvadj  31964  rinvf1o  32703  isconstr  33880  bnj97  35008  bnj150  35018  bnj1384  35174  bnj1421  35184  bnj60  35204  satffunlem2lem2  35588  satfv0fvfmla0  35595  funpartfun  36125  funtransport  36213  funray  36322  funline  36324  modelaxreplem2  45406  xlimfun  46283  funcoressn  47490  upgrimpthslem1  48383  upgrimspths  48386