Theorem funss 5611

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

Step	Hyp	Ref	Expression
1		relss 5095	. . 3
2		coss1 5163	. . . . 5
3		cnvss 5180	. . . . . 6
4		coss2 5164	. . . . . 6
5	3, 4	syl 16	. . . . 5
6	2, 5	sstrd 3513	. . . 4
7		sstr2 3510	. . . 4
8	6, 7	syl 16	. . 3
9	1, 8	anim12d 563	. 2
10		df-fun 5595	. 2
11		df-fun 5595	. 2
12	9, 10, 11	3imtr4g 270	1

Syntax hints:  ->wi 4  /\wa 369  C_wss 3475  cid 4795  `'ccnv 5003  o.ccom 5008  Relwrel 5009  Funwfun 5587

This theorem is referenced by:  funeq  5612  funopab4  5628  funres  5632  fun0  5650  funcnvcnv  5651  funin  5660  funres11  5661  foimacnv  5838  funsssuppss  6945  strssd  14668  strle1  14728  xpsc0  14957  xpsc1  14958  pjpm  18739  frrlem5c  29393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-fun 5595