Theorem funeqi 5909

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

Syntax hints:   ↔ wb 196   = wceq 1483  Fun wfun 5882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-br 4654  df-opab 4713  df-rel 5121  df-cnv 5122  df-co 5123  df-fun 5890

This theorem is referenced by:  funmpt  5926  funmpt2  5927  funco  5928  fununfun  5934  funprg  5940  funprgOLD  5941  funtpg  5942  funtpgOLD  5943  funtp  5945  funcnvpr  5950  funcnvtp  5951  funcnvqp  5952  funcnvqpOLD  5953  funcnv0  5955  f1cnvcnv  6109  f1co  6110  f10  6169  opabiotafun  6259  fvn0ssdmfun  6350  funopdmsn  6415  fpropnf1  6524  funoprabg  6759  mpt2fun  6762  ovidig  6778  funcnvuni  7119  fun11iun  7126  tposfun  7368  tfr1a  7490  tz7.44lem1  7501  tz7.48-2  7537  ssdomg  8001  sbthlem7  8076  sbthlem8  8077  1sdom  8163  hartogslem1  8447  r1funlim  8629  zorn2lem4  9321  axaddf  9966  axmulf  9967  fundmge2nop0  13274  funcnvs1  13657  strlemor1OLD  15969  strleun  15972  fthoppc  16583  cnfldfun  19758  cnfldfunALT  19759  volf  23297  dfrelog  24312  usgredg3  26108  ushgredgedg  26121  ushgredgedgloop  26123  2trld  26834  0pth  26986  1pthdlem1  26995  1trld  27002  3trld  27032  ajfuni  27715  hlimf  28094  funadj  28745  funcnvadj  28752  rinvf1o  29432  funcnvmptOLD  29467  bnj97  30936  bnj150  30946  bnj1384  31100  bnj1421  31110  bnj60  31130  frrlem10  31791  funpartfun  32050  funtransport  32138  funray  32247  funline  32249  funresfunco  41205  funcoressn  41207