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

Theorem funeq 6374
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 4028 . . 3 (𝐴 = 𝐵𝐵𝐴)
2 funss 6373 . . 3 (𝐵𝐴 → (Fun 𝐴 → Fun 𝐵))
31, 2syl 17 . 2 (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4 eqimss 4027 . . 3 (𝐴 = 𝐵𝐴𝐵)
5 funss 6373 . . 3 (𝐴𝐵 → (Fun 𝐵 → Fun 𝐴))
64, 5syl 17 . 2 (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
73, 6impbid 213 1 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  wss 3940  Fun wfun 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-in 3947  df-ss 3956  df-br 5064  df-opab 5126  df-rel 5561  df-cnv 5562  df-co 5563  df-fun 6356
This theorem is referenced by:  funeqi  6375  funeqd  6376  fununi  6428  cnvresid  6432  fneq1  6443  funop  6909  funsndifnop  6911  nvof1o  7033  funcnvuni  7629  fiunw  7637  fiun  7640  elpmg  8417  fundmeng  8578  isfsupp  8831  dfac9  9556  axdc3lem2  9867  frlmphllem  20859  usgredgop  26888  locfinreflem  31009  orvcval  31620  bnj1379  32007  bnj1385  32009  bnj1497  32235  funen1cnv  32260  elfunsg  33280  funop1  43367
  Copyright terms: Public domain W3C validator