Theorem relss 4819

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 3235	. 2 |- ( A C_ B -> ( B C_ ( _V X. _V ) -> A C_ ( _V X. _V ) ) )
2		df-rel 4738	. 2 |- ( Rel B <-> B C_ ( _V X. _V ) )
3		df-rel 4738	. 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 2803   C_ wss 3201   X. cxp 4729   Rel wrel 4736

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214  df-rel 4738

This theorem is referenced by:  relin1  4851  relin2  4852  reldif  4853  relres  5047  iss  5065  cnvdif  5150  funss  5352  funssres  5376  fliftcnv  5946  fliftfun  5947  reltpos  6459  tpostpos  6473  swoer  6773  erinxp  6821  ltrel  8300  lerel  8302  txdis1cn  15089  xmeter  15247  lgsquadlem1  15896  lgsquadlem2  15897