Theorem ssbrd 4493

Description: Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)

Hypothesis

Ref	Expression
ssbrd.1

Assertion

Ref	Expression
ssbrd

Proof of Theorem ssbrd

Step	Hyp	Ref	Expression
1		ssbrd.1	. . 3
2	1	sseld 3502	. 2
3		df-br 4453	. 2
4		df-br 4453	. 2
5	2, 3, 4	3imtr4g 270	1

Syntax hints:  ->wi 4  e.wcel 1818  C_wss 3475  <.cop 4035   class class class wbr 4452

This theorem is referenced by:  ssbri  4494  sess1  4852  brrelex12  5042  coss1  5163  coss2  5164  eqbrrdva  5177  ersym  7342  ertr  7345  fpwwe2lem6  9034  fpwwe2lem7  9035  fpwwe2lem9  9037  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  fthres2  15301  invfuc  15343  pospo  15603  dirref  15865  efgcpbl  16774  frgpuplem  16790  subrguss  17444  znleval  18593  ustref  20721  ustuqtop4  20747  isucn2  20782  brelg  27462  metider  27873  mclsppslem  28943  fundmpss  29196  coss12d  37759

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-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-br 4453