Theorem relss 4763

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 3200	. 2 |- ( A C_ B -> ( B C_ ( _V X. _V ) -> A C_ ( _V X. _V ) ) )
2		df-rel 4683	. 2 |- ( Rel B <-> B C_ ( _V X. _V ) )
3		df-rel 4683	. 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 2772   C_ wss 3166   X. cxp 4674   Rel wrel 4681

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179  df-rel 4683

This theorem is referenced by:  relin1  4794  relin2  4795  reldif  4796  relres  4988  iss  5006  cnvdif  5090  funss  5291  funssres  5314  fliftcnv  5866  fliftfun  5867  reltpos  6338  tpostpos  6352  swoer  6650  erinxp  6698  ltrel  8136  lerel  8138  txdis1cn  14783  xmeter  14941  lgsquadlem1  15587  lgsquadlem2  15588