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

Theorem funeq 6355
 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 3949 . . 3 (𝐴 = 𝐵𝐵𝐴)
2 funss 6354 . . 3 (𝐵𝐴 → (Fun 𝐴 → Fun 𝐵))
31, 2syl 17 . 2 (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4 eqimss 3948 . . 3 (𝐴 = 𝐵𝐴𝐵)
5 funss 6354 . . 3 (𝐴𝐵 → (Fun 𝐵 → Fun 𝐴))
64, 5syl 17 . 2 (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
73, 6impbid 215 1 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ⊆ wss 3858  Fun wfun 6329 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-br 5033  df-opab 5095  df-rel 5531  df-cnv 5532  df-co 5533  df-fun 6337 This theorem is referenced by:  funeqi  6356  funeqd  6357  fununi  6410  cnvresid  6414  fneq1  6425  funop  6902  funsndifnop  6904  nvof1o  7029  funcnvuni  7641  fiun  7648  elpmg  8432  fundmeng  8603  isfsupp  8870  dfac9  9596  axdc3lem2  9911  frlmphllem  20545  usgredgop  27062  locfinreflem  31311  orvcval  31943  bnj1379  32330  bnj1385  32332  bnj1497  32560  funen1cnv  32585  oldval  33598  elfunsg  33767  funop1  44207
 Copyright terms: Public domain W3C validator