Theorem relss 4699

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

Syntax hints:   -> wi 4   _Vcvv 2731   C_ wss 3122   X. cxp 4610   Rel wrel 4617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-11 1500  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-in 3128  df-ss 3135  df-rel 4619

This theorem is referenced by:  relin1  4730  relin2  4731  reldif  4732  relres  4920  iss  4938  cnvdif  5019  funss  5219  funssres  5242  fliftcnv  5778  fliftfun  5779  reltpos  6233  tpostpos  6247  swoer  6545  erinxp  6591  ltrel  7985  lerel  7987  txdis1cn  13157  xmeter  13315