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

Theorem funeq 6121
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 3855 . . 3 (𝐴 = 𝐵𝐵𝐴)
2 funss 6120 . . 3 (𝐵𝐴 → (Fun 𝐴 → Fun 𝐵))
31, 2syl 17 . 2 (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4 eqimss 3854 . . 3 (𝐴 = 𝐵𝐴𝐵)
5 funss 6120 . . 3 (𝐴𝐵 → (Fun 𝐵 → Fun 𝐴))
64, 5syl 17 . 2 (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
73, 6impbid 203 1 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wss 3769  Fun wfun 6095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-in 3776  df-ss 3783  df-br 4845  df-opab 4907  df-rel 5318  df-cnv 5319  df-co 5320  df-fun 6103
This theorem is referenced by:  funeqi  6122  funeqd  6123  fununi  6175  cnvresid  6179  fneq1  6190  funop  6638  funsndifnop  6640  nvof1o  6760  funcnvuni  7349  elpmg  8108  fundmeng  8267  isfsupp  8518  dfac9  9243  axdc3lem2  9558  frlmphllem  20329  usgredgop  26280  locfinreflem  30232  orvcval  30844  bnj1379  31224  bnj1385  31226  bnj1497  31451  elfunsg  32344  funop1  41873
  Copyright terms: Public domain W3C validator