Theorem funeqi 5102

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

Hypothesis

Ref	Expression
funeqi.1	|- A = B

Assertion

Ref	Expression
funeqi	|- ( Fun A <-> Fun B )

Proof of Theorem funeqi

Step	Hyp	Ref	Expression
1		funeqi.1	. 2 |- A = B
2		funeq 5101	. 2 |- ( A = B -> ( Fun A <-> Fun B ) )
3	1, 2	ax-mp 7	1 |- ( Fun A <-> Fun B )

Syntax hints:   <-> wb 104   = wceq 1314   Fun wfun 5075

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-in 3043  df-ss 3050  df-br 3896  df-opab 3950  df-rel 4506  df-cnv 4507  df-co 4508  df-fun 5083

This theorem is referenced by:  funmpt  5119  funmpt2  5120  funprg  5131  funtpg  5132  funtp  5134  funcnvuni  5150  f1cnvcnv  5297  f1co  5298  fun11iun  5344  f10  5357  funoprabg  5824  mpofun  5827  ovidig  5842  tposfun  6111  tfri1dALT  6202  tfrcl  6215  rdgfun  6224  frecfun  6246  frecfcllem  6255  th3qcor  6487  ssdomg  6626  sbthlem7  6803  sbthlemi8  6804  casefun  6922  caseinj  6926  djufun  6941  djuinj  6943  ctssdccl  6948  axaddf  7600  axmulf  7601  strleund  11887  strleun  11888  1strbas  11898  2strbasg  11900  2stropg  11901