Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  funss Structured version   Unicode version

Theorem funss 5474
 Description: Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
Assertion
Ref Expression
funss

Proof of Theorem funss
StepHypRef Expression
1 relss 4965 . . 3
2 coss1 5030 . . . . 5
3 cnvss 5047 . . . . . 6
4 coss2 5031 . . . . . 6
53, 4syl 16 . . . . 5
62, 5sstrd 3360 . . . 4
7 sstr2 3357 . . . 4
86, 7syl 16 . . 3
91, 8anim12d 548 . 2
10 df-fun 5458 . 2
11 df-fun 5458 . 2
129, 10, 113imtr4g 263 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 360   wss 3322   cid 4495  ccnv 4879   ccom 4884   wrel 4885   wfun 5450 This theorem is referenced by:  funeq  5475  funopab4  5490  funres  5494  fun0  5510  funcnvcnv  5511  funin  5522  funres11  5523  foimacnv  5694  strssd  13505  strle1  13562  xpsc0  13787  xpsc1  13788  pjpm  16937  frrlem5c  25590 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-in 3329  df-ss 3336  df-br 4215  df-opab 4269  df-rel 4887  df-cnv 4888  df-co 4889  df-fun 5458
 Copyright terms: Public domain W3C validator