Theorem funeqi 6484

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

Syntax hints:   ↔ wb 205   = wceq 1539  Fun wfun 6452

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909  df-br 5082  df-opab 5144  df-rel 5607  df-cnv 5608  df-co 5609  df-fun 6460

This theorem is referenced by:  funmpt  6501  funmpt2  6502  funco  6503  funresfunco  6504  fununfun  6511  funprg  6517  funtpg  6518  funtp  6520  funcnvpr  6525  funcnvtp  6526  funcnvqp  6527  funcnv0  6529  f1cnvcnv  6710  f1cof1  6711  f1coOLD  6713  opabiotafun  6881  fvn0ssdmfun  6984  funopdmsn  7054  fpropnf1  7172  funoprabg  7427  mpofun  7430  mpofunOLD  7431  ovidig  7447  funcnvuni  7810  fiun  7817  f1iun  7818  tposfun  8089  tfr1a  8256  tz7.44lem1  8267  tz7.48-2  8304  ssdomg  8821  sbthlem7  8914  sbthlem8  8915  1sdomOLD  9070  hartogslem1  9349  r1funlim  9572  zorn2lem4  10305  axaddf  10951  axmulf  10952  fundmge2nop0  14255  funcnvs1  14674  strleun  16907  fthoppc  17688  cnfldfun  20658  cnfldfunALT  20659  cnfldfunALTOLD  20660  volf  24742  dfrelog  25770  usgredg3  27632  ushgredgedg  27645  ushgredgedgloop  27647  2trld  28352  0pth  28538  1pthdlem1  28548  1trld  28555  3trld  28585  ajfuni  29270  hlimf  29648  funadj  30297  funcnvadj  30304  rinvf1o  31014  bnj97  32895  bnj150  32905  bnj1384  33061  bnj1421  33071  bnj60  33091  satffunlem2lem2  33417  satfv0fvfmla0  33424  funpartfun  34294  funtransport  34382  funray  34491  funline  34493  xlimfun  43625  funcoressn  44780