Theorem funeqi 6587

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-rel 5692  df-cnv 5693  df-co 5694  df-fun 6563

This theorem is referenced by:  funmpt  6604  funmpt2  6605  funco  6606  funresfunco  6607  fununfun  6614  funprg  6620  funtpg  6621  funtp  6623  funcnvpr  6628  funcnvtp  6629  funcnvqp  6630  funcnv0  6632  f1cnvcnv  6813  f1cof1  6814  opabiotafun  6989  fvn0ssdmfun  7094  funopdmsn  7170  fpropnf1  7287  funoprabg  7554  mpofun  7557  ovidig  7575  funcnvuni  7954  resf1extb  7956  fiun  7967  f1iun  7968  tposfun  8267  tfr1a  8434  tz7.44lem1  8445  tz7.48-2  8482  ssdomg  9040  sbthlem7  9129  sbthlem8  9130  1sdomOLD  9285  hartogslem1  9582  r1funlim  9806  zorn2lem4  10539  axaddf  11185  axmulf  11186  fundmge2nop0  14541  funcnvs1  14951  strleun  17194  fthoppc  17970  cnfldfun  21378  cnfldfunALT  21379  cnfldfunOLD  21391  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  volf  25564  dfrelog  26607  precsexlem10  28240  precsexlem11  28241  usgredg3  29233  ushgredgedg  29246  ushgredgedgloop  29248  2trld  29958  0pth  30144  1pthdlem1  30154  1trld  30161  3trld  30191  ajfuni  30878  hlimf  31256  funadj  31905  funcnvadj  31912  rinvf1o  32640  isconstr  33777  bnj97  34880  bnj150  34890  bnj1384  35046  bnj1421  35056  bnj60  35076  satffunlem2lem2  35411  satfv0fvfmla0  35418  funpartfun  35944  funtransport  36032  funray  36141  funline  36143  modelaxreplem2  44996  xlimfun  45870  funcoressn  47054