Theorem funeqi 6570

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

Syntax hints:   ↔ wb 205   = wceq 1542  Fun wfun 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-rel 5684  df-cnv 5685  df-co 5686  df-fun 6546

This theorem is referenced by:  funmpt  6587  funmpt2  6588  funco  6589  funresfunco  6590  fununfun  6597  funprg  6603  funtpg  6604  funtp  6606  funcnvpr  6611  funcnvtp  6612  funcnvqp  6613  funcnv0  6615  f1cnvcnv  6798  f1cof1  6799  f1coOLD  6801  opabiotafun  6973  fvn0ssdmfun  7077  funopdmsn  7148  fpropnf1  7266  funoprabg  7529  mpofun  7532  mpofunOLD  7533  ovidig  7550  funcnvuni  7922  fiun  7929  f1iun  7930  tposfun  8227  tfr1a  8394  tz7.44lem1  8405  tz7.48-2  8442  ssdomg  8996  sbthlem7  9089  sbthlem8  9090  1sdomOLD  9249  hartogslem1  9537  r1funlim  9761  zorn2lem4  10494  axaddf  11140  axmulf  11141  fundmge2nop0  14453  funcnvs1  14863  strleun  17090  fthoppc  17874  cnfldfun  20956  cnfldfunALT  20957  cnfldfunALTOLD  20958  volf  25046  dfrelog  26074  precsexlem10  27665  precsexlem11  27666  usgredg3  28504  ushgredgedg  28517  ushgredgedgloop  28519  2trld  29223  0pth  29409  1pthdlem1  29419  1trld  29426  3trld  29456  ajfuni  30143  hlimf  30521  funadj  31170  funcnvadj  31177  rinvf1o  31885  bnj97  33908  bnj150  33918  bnj1384  34074  bnj1421  34084  bnj60  34104  satffunlem2lem2  34428  satfv0fvfmla0  34435  funpartfun  34946  funtransport  35034  funray  35143  funline  35145  gg-cnfldfun  35228  gg-cnfldfunALT  35229  xlimfun  44619  funcoressn  45800