Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  funeqi GIF version

Theorem funeqi 5112
 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
StepHypRef Expression
1 funeqi.1 . 2 𝐴 = 𝐵
2 funeq 5111 . 2 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
31, 2ax-mp 5 1 (Fun 𝐴 ↔ Fun 𝐵)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   = wceq 1314  Fun wfun 5085 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-in 3045  df-ss 3052  df-br 3898  df-opab 3958  df-rel 4514  df-cnv 4515  df-co 4516  df-fun 5093 This theorem is referenced by:  funmpt  5129  funmpt2  5130  funprg  5141  funtpg  5142  funtp  5144  funcnvuni  5160  f1cnvcnv  5307  f1co  5308  fun11iun  5354  f10  5367  funoprabg  5836  mpofun  5839  ovidig  5854  tposfun  6123  tfri1dALT  6214  tfrcl  6227  rdgfun  6236  frecfun  6258  frecfcllem  6267  th3qcor  6499  ssdomg  6638  sbthlem7  6817  sbthlemi8  6818  casefun  6936  caseinj  6940  djufun  6955  djuinj  6957  ctssdccl  6962  axaddf  7640  axmulf  7641  strleund  11942  strleun  11943  1strbas  11953  2strbasg  11955  2stropg  11956
 Copyright terms: Public domain W3C validator