Theorem funeqi 5373

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

Syntax hints:   ↔ wb 105   = wceq 1398  Fun wfun 5346

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 3217  df-ss 3224  df-br 4110  df-opab 4172  df-rel 4756  df-cnv 4757  df-co 4758  df-fun 5354

This theorem is referenced by:  funmpt  5390  funmpt2  5391  fununfun  5399  funprg  5406  funtpg  5407  funtp  5409  funcnvuni  5425  f1cnvcnv  5584  f1co  5585  fun11iun  5635  f10  5649  funopdmsn  5864  funoprabg  6152  mpofun  6155  ovidig  6171  tposfun  6491  tfri1dALT  6582  tfrcl  6595  rdgfun  6604  frecfun  6626  frecfcllem  6635  th3qcor  6873  ssdomg  7018  sbthlem7  7233  sbthlemi8  7234  casefun  7376  caseinj  7380  djufun  7395  djuinj  7397  ctssdccl  7402  axaddf  8183  axmulf  8184  fundm2domnop0  11220  strleund  13316  strleun  13317  1strbas  13330  2strbasg  13333  2stropg  13334  lidlmex  14623  usgredg3  16209  ushgredgedg  16221  ushgredgedgloop  16223