Theorem relss 4933

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 3468	. 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 273	1 |- ( A C_ B -> ( Rel B -> Rel A ) )

Syntax hints:   -> wi 4   _Vcvv 3078   C_ wss 3433   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 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447  df-rel 4852

This theorem is referenced by:  relin1  4962  relin2  4963  reldif  4964  relres  5143  iss  5163  cnvdif  5253  difxp  5272  sofld  5295  funss  5610  funssres  5632  fliftcnv  6210  fliftfun  6211  frxp  6908  reltpos  6977  tpostpos  6992  swoer  7390  erinxp  7436  sbthcl  7691  fpwwe2lem8  9051  fpwwe2lem9  9052  fpwwe2lem12  9055  recmulnq  9378  prcdnq  9407  ltrel  9685  lerel  9687  dfle2  11435  dflt2  11436  pwsle  15342  isinv  15609  invsym2  15612  invfun  15613  oppcsect2  15628  oppcinv  15629  relfull  15757  relfth  15758  psss  16404  gicer  16884  gsum2d  17532  isunit  17813  opsrtoslem2  18636  txdis1cn  20574  hmpher  20723  tgphaus  21055  qustgplem  21059  tsmsxp  21093  xmeter  21372  ovoliunlem1  22349  taylf  23207  lgsquadlem1  24171  lgsquadlem2  24172  nvrel  26092  phrel  26327  bnrel  26380  hlrel  26403  elrn3  30216  sscoid  30491  trer  30783  fneer  30820  heicant  31708  dvhopellsm  34423  diclspsn  34500  dih1dimatlem  34635