Theorem relss 5090

Description: Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)

Assertion

Ref	Expression
relss	|- ( A C_ B -> ( Rel B -> Rel A ) )

Proof of Theorem relss

Step	Hyp	Ref	Expression
1		sstr2 3511	. 2 |- ( A C_ B -> ( B C_ ( _V X. _V ) -> A C_ ( _V X. _V ) ) )
2		df-rel 5006	. 2 |- ( Rel B <-> B C_ ( _V X. _V ) )
3		df-rel 5006	. 2 |- ( Rel A <-> A C_ ( _V X. _V ) )
4	1, 2, 3	3imtr4g 270	1 |- ( A C_ B -> ( Rel B -> Rel A ) )

Syntax hints:   -> wi 4   _Vcvv 3113   C_ wss 3476   X. cxp 4997   Rel wrel 5004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-rel 5006

This theorem is referenced by:  relin1  5120  relin2  5121  reldif  5122  relres  5301  iss  5321  cnvdif  5412  difxp  5431  sofld  5455  funss  5606  funssres  5628  fliftcnv  6197  fliftfun  6198  frxp  6893  reltpos  6960  tpostpos  6975  swoer  7339  erinxp  7385  sbthcl  7639  fpwwe2lem8  9015  fpwwe2lem9  9016  fpwwe2lem12  9019  recmulnq  9342  prcdnq  9371  ltrel  9649  lerel  9651  dfle2  11353  dflt2  11354  pwsle  14747  isinv  15015  invsym2  15018  invfun  15019  oppcsect2  15030  oppcinv  15031  relfull  15135  relfth  15136  psss  15701  gicer  16129  gsum2d  16802  gsum2dOLD  16803  isunit  17107  opsrtoslem2  17948  txdis1cn  19899  hmpher  20048  tgphaus  20378  divstgplem  20382  tsmsxp  20420  xmeter  20699  ovoliunlem1  21676  taylf  22518  lgsquadlem1  23385  lgsquadlem2  23386  nvrel  25199  phrel  25434  bnrel  25487  hlrel  25510  elrn3  28797  sscoid  29168  heicant  29654  trer  29739  fneer  29788  dvhopellsm  35932  diclspsn  36009  dih1dimatlem  36144