Theorem funeqi 5613

Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
funeqi.1

Assertion

Ref	Expression
funeqi

Proof of Theorem funeqi

Step	Hyp	Ref	Expression
1		funeqi.1	. 2
2		funeq 5612	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  <->wb 184  =wceq 1395  Funwfun 5587

This theorem is referenced by:  funmpt  5629  funmpt2  5630  funco  5631  fununfun  5637  funprg  5642  funtpg  5643  funtp  5645  f1cnvcnv  5794  f1co  5795  f10  5852  opabiotafun  5934  fvn0ssdmfun  6022  funoprabg  6401  mpt2fun  6404  ovidig  6420  funcnvuni  6753  fun11iun  6760  tposfun  6990  tfr1a  7082  tz7.44lem1  7090  tz7.48-2  7126  ssdomg  7581  sbthlem7  7653  sbthlem8  7654  1sdom  7742  hartogslem1  7988  r1funlim  8205  zorn2lem4  8900  axaddf  9543  axmulf  9544  structfun  14644  strlemor1  14724  strleun  14727  fthoppc  15292  volf  21940  dfrelog  22953  0trl  24548  0pth  24572  1pthonlem1  24591  2pthlem1  24597  ajfuni  25775  hlimf  26155  funadj  26805  funcnvadj  26812  rinvf1o  27472  funcnvmptOLD  27509  frrlem10  29398  funpartfun  29593  funtransport  29681  funray  29790  funline  29792  funresfunco  32210  funcoressn  32212  bnj97  33924  bnj150  33934  bnj1384  34088  bnj1421  34098  bnj60  34118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-fun 5595