Theorem relss 4927

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 3425	. 2 |- ( A C_ B -> ( B C_ ( _V X. _V ) -> A C_ ( _V X. _V ) ) )
2		df-rel 4846	. 2 |- ( Rel B <-> B C_ ( _V X. _V ) )
3		df-rel 4846	. 2 |- ( Rel A <-> A C_ ( _V X. _V ) )
4	1, 2, 3	3imtr4g 278	1 |- ( A C_ B -> ( Rel B -> Rel A ) )

Syntax hints:   -> wi 4   _Vcvv 3031   C_ wss 3390   X. cxp 4837   Rel wrel 4844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404  df-rel 4846

This theorem is referenced by:  relin1  4956  relin2  4957  reldif  4958  relres  5138  iss  5158  cnvdif  5248  difxp  5267  sofld  5290  funss  5607  funssres  5629  fliftcnv  6222  fliftfun  6223  frxp  6925  reltpos  6996  tpostpos  7011  swoer  7409  erinxp  7455  sbthcl  7712  fpwwe2lem8  9080  fpwwe2lem9  9081  fpwwe2lem12  9084  recmulnq  9407  prcdnq  9436  ltrel  9714  lerel  9716  dfle2  11469  dflt2  11470  pwsle  15468  isinv  15743  invsym2  15746  invfun  15747  oppcsect2  15762  oppcinv  15763  relfull  15891  relfth  15892  psss  16538  gicer  17018  gsum2d  17682  isunit  17963  opsrtoslem2  18785  txdis1cn  20727  hmpher  20876  tgphaus  21209  qustgplem  21213  tsmsxp  21247  xmeter  21526  ovoliunlem1  22533  taylf  23395  lgsquadlem1  24361  lgsquadlem2  24362  nvrel  26302  phrel  26537  bnrel  26590  hlrel  26623  elrn3  30474  sscoid  30751  trer  31043  fneer  31080  heicant  32039  dvhopellsm  34756  diclspsn  34833  dih1dimatlem  34968