Theorem relss 4932

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 3368	. 2 |- ( A C_ B -> ( B C_ ( _V X. _V ) -> A C_ ( _V X. _V ) ) )
2		df-rel 4852	. 2 |- ( Rel B <-> B C_ ( _V X. _V ) )
3		df-rel 4852	. 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 2977   C_ wss 3333   X. cxp 4843   Rel wrel 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3340  df-ss 3347  df-rel 4852

This theorem is referenced by:  relin1  4962  relin2  4963  reldif  4964  relres  5143  iss  5159  cnvdif  5248  difxp  5267  sofld  5291  funss  5441  funssres  5463  fliftcnv  6009  fliftfun  6010  frxp  6687  reltpos  6755  tpostpos  6770  swoer  7134  erinxp  7179  sbthcl  7438  fpwwe2lem8  8809  fpwwe2lem9  8810  fpwwe2lem12  8813  recmulnq  9138  prcdnq  9167  ltrel  9444  lerel  9446  dfle2  11129  dflt2  11130  pwsle  14435  isinv  14703  invsym2  14706  invfun  14707  oppcsect2  14718  oppcinv  14719  relfull  14823  relfth  14824  psss  15389  gicer  15809  gsum2d  16468  gsum2dOLD  16469  isunit  16754  opsrtoslem2  17571  txdis1cn  19213  hmpher  19362  tgphaus  19692  divstgplem  19696  tsmsxp  19734  xmeter  20013  ovoliunlem1  20990  taylf  21831  lgsquadlem1  22698  lgsquadlem2  22699  nvrel  23985  phrel  24220  bnrel  24273  hlrel  24296  elrn3  27578  sscoid  27949  heicant  28431  trer  28516  fneer  28565  dvhopellsm  34767  diclspsn  34844  dih1dimatlem  34979