Theorem funeqi 5291

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

Syntax hints:   ↔ wb 105   = wceq 1372  Fun wfun 5264

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-in 3171  df-ss 3178  df-br 4044  df-opab 4105  df-rel 4681  df-cnv 4682  df-co 4683  df-fun 5272

This theorem is referenced by:  funmpt  5308  funmpt2  5309  fununfun  5316  funprg  5323  funtpg  5324  funtp  5326  funcnvuni  5342  f1cnvcnv  5491  f1co  5492  fun11iun  5542  f10  5555  funopdmsn  5763  funoprabg  6043  mpofun  6046  ovidig  6062  tposfun  6345  tfri1dALT  6436  tfrcl  6449  rdgfun  6458  frecfun  6480  frecfcllem  6489  th3qcor  6725  ssdomg  6869  sbthlem7  7064  sbthlemi8  7065  casefun  7186  caseinj  7190  djufun  7205  djuinj  7207  ctssdccl  7212  axaddf  7980  axmulf  7981  fundm2domnop0  10988  strleund  12906  strleun  12907  1strbas  12920  2strbasg  12923  2stropg  12924  lidlmex  14208