Theorem funeqi 6568

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  Fun wfun 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3900  df-br 5106  df-opab 5170  df-rel 5661  df-cnv 5662  df-co 5663  df-fun 6548

This theorem is used by:  funmpt  6586  funmpt2  6587  funco  6588  funresfunco  6589  fununfun  6596  funprg  6602  funtpg  6603  funtp  6605  funcnvpr  6610  funcnvtp  6611  funcnvqp  6612  funcnv0  6614  f1cnvcnv  6797  f1cof1  6798  f1oi  6871  opabiotafun  6973  fvn0ssdmfun  7082  funopdmsn  7162  fpropnf1  7278  funoprabg  7548  mpofun  7551  ovidig  7569  funmpt3  7694  funcnvuni  7951  resf1extb  7953  fiun  7962  f1iun  7963  tposfun  8270  tfr1a  8413  tz7.44lem1  8424  tz7.48-2  8463  ssdomg  9038  sbthlem7  9123  sbthlem8  9124  hartogslem1  9546  r1funlimOLD  9780  r1fun  9781  zorn2lem4  10587  axaddf  11240  axmulf  11241  fundmge2nop0  14657  funcnvs1  15075  strleun  17347  fthoppc  18112  mgmn0plusgf  18839  degenmgm2nfun  19151  cnfldfun  21704  cnfldfunALT  21705  volf  25862  dfrelog  26905  precsexlem10  28614  precsexlem11  28615  usgredg3  29809  ushgredgedg  29822  ushgredgedgloop  29824  2trld  30539  0pth  30728  1pthdlem1  30738  1trld  30745  3trld  30785  ajfuni  31473  hlimf  31851  funadj  32500  funcnvadj  32507  rinvf1o  33278  isconstr  34421  bnj97  35549  bnj150  35559  bnj1384  35715  bnj1421  35725  bnj60  35745  fwfffun  35770  srepdflem1  36039  srepdflem2  36040  satffunlem2lem2  36292  satfv0fvfmla0  36299  funpartfun  36834  funtransport  36923  funray  37032  funline  37034  modelaxreplem2  46108  xlimfun  47004  funcoressn  48251  upgrimpthslem1  49144  upgrimspths  49147