Theorem funeqi 5372

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

Syntax hints:   <-> wb 105   = wceq 1398   Fun wfun 5345

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-in 3216  df-ss 3223  df-br 4109  df-opab 4171  df-rel 4755  df-cnv 4756  df-co 4757  df-fun 5353

This theorem is referenced by:  funmpt  5389  funmpt2  5390  fununfun  5398  funprg  5405  funtpg  5406  funtp  5408  funcnvuni  5424  f1cnvcnv  5583  f1co  5584  fun11iun  5634  f10  5648  funopdmsn  5863  funoprabg  6151  mpofun  6154  ovidig  6170  tposfun  6490  tfri1dALT  6581  tfrcl  6594  rdgfun  6603  frecfun  6625  frecfcllem  6634  th3qcor  6872  ssdomg  7017  sbthlem7  7232  sbthlemi8  7233  casefun  7375  caseinj  7379  djufun  7394  djuinj  7396  ctssdccl  7401  axaddf  8179  axmulf  8180  fundm2domnop0  11213  strleund  13305  strleun  13306  1strbas  13319  2strbasg  13322  2stropg  13323  lidlmex  14610  usgredg3  16196  ushgredgedg  16208  ushgredgedgloop  16210