Theorem funeqi 5349

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 5348	. 2 |- ( A = B -> ( Fun A <-> Fun B ) )
3	1, 2	ax-mp 5	1 |- ( Fun A <-> Fun B )

Syntax hints:   <-> wb 105   = wceq 1397   Fun wfun 5322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-in 3205  df-ss 3212  df-br 4090  df-opab 4152  df-rel 4734  df-cnv 4735  df-co 4736  df-fun 5330

This theorem is referenced by:  funmpt  5366  funmpt2  5367  fununfun  5375  funprg  5382  funtpg  5383  funtp  5385  funcnvuni  5401  f1cnvcnv  5556  f1co  5557  fun11iun  5607  f10  5621  funopdmsn  5837  funoprabg  6125  mpofun  6128  ovidig  6144  tposfun  6431  tfri1dALT  6522  tfrcl  6535  rdgfun  6544  frecfun  6566  frecfcllem  6575  th3qcor  6813  ssdomg  6957  sbthlem7  7167  sbthlemi8  7168  casefun  7289  caseinj  7293  djufun  7308  djuinj  7310  ctssdccl  7315  axaddf  8093  axmulf  8094  fundm2domnop0  11118  strleund  13209  strleun  13210  1strbas  13223  2strbasg  13226  2stropg  13227  lidlmex  14513  usgredg3  16094  ushgredgedg  16106  ushgredgedgloop  16108