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

Theorem funeq 6586
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 4043 . . 3 (𝐴 = 𝐵𝐵𝐴)
2 funss 6585 . . 3 (𝐵𝐴 → (Fun 𝐴 → Fun 𝐵))
31, 2syl 17 . 2 (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4 eqimss 4042 . . 3 (𝐴 = 𝐵𝐴𝐵)
5 funss 6585 . . 3 (𝐴𝐵 → (Fun 𝐵 → Fun 𝐴))
64, 5syl 17 . 2 (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
73, 6impbid 212 1 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wss 3951  Fun wfun 6555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-rel 5692  df-cnv 5693  df-co 5694  df-fun 6563
This theorem is referenced by:  funeqi  6587  funeqd  6588  fununi  6641  cnvresid  6645  fneq1  6659  funop  7169  funsndifnop  7171  nvof1o  7300  funcnvuni  7954  fiun  7967  elpmg  8883  fundmeng  9072  isfsupp  9405  dfac9  10177  axdc3lem2  10491  frlmphllem  21800  psdmul  22170  oldval  27893  usgredgop  29187  locfinreflem  33839  orvcval  34460  bnj1379  34844  bnj1385  34846  bnj1497  35074  funen1cnv  35102  elfunsg  35917  modelaxreplem1  44995  modelaxreplem2  44996  modelaxrep  44998  funop1  47295
  Copyright terms: Public domain W3C validator