MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funeq Structured version   Visualization version   GIF version

Theorem funeq 6522
Description: Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
Assertion
Ref Expression
funeq (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))

Proof of Theorem funeq
StepHypRef Expression
1 eqimss2 4002 . . 3 (𝐴 = 𝐵𝐵𝐴)
2 funss 6521 . . 3 (𝐵𝐴 → (Fun 𝐴 → Fun 𝐵))
31, 2syl 17 . 2 (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4 eqimss 4001 . . 3 (𝐴 = 𝐵𝐴𝐵)
5 funss 6521 . . 3 (𝐴𝐵 → (Fun 𝐵 → Fun 𝐴))
64, 5syl 17 . 2 (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
73, 6impbid 211 1 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wss 3911  Fun wfun 6491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-br 5107  df-opab 5169  df-rel 5641  df-cnv 5642  df-co 5643  df-fun 6499
This theorem is referenced by:  funeqi  6523  funeqd  6524  fununi  6577  cnvresid  6581  fneq1  6594  funop  7096  funsndifnop  7098  nvof1o  7227  funcnvuni  7869  fiun  7876  elpmg  8784  fundmeng  8979  isfsupp  9312  dfac9  10077  axdc3lem2  10392  frlmphllem  21202  oldval  27206  usgredgop  28163  locfinreflem  32478  orvcval  33114  bnj1379  33499  bnj1385  33501  bnj1497  33729  funen1cnv  33749  elfunsg  34547  funop1  45601
  Copyright terms: Public domain W3C validator