Theorem relss 4727

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

Syntax hints:   -> wi 4   _Vcvv 2751   C_ wss 3143   X. cxp 4638   Rel wrel 4645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-in 3149  df-ss 3156  df-rel 4647

This theorem is referenced by:  relin1  4758  relin2  4759  reldif  4760  relres  4949  iss  4967  cnvdif  5049  funss  5249  funssres  5272  fliftcnv  5811  fliftfun  5812  reltpos  6268  tpostpos  6282  swoer  6580  erinxp  6626  ltrel  8036  lerel  8038  txdis1cn  14161  xmeter  14319