Theorem relss 4762

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 4682	. 2 |- ( Rel B <-> B C_ ( _V X. _V ) )
3		df-rel 4682	. 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 4673   Rel wrel 4680

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 4682

This theorem is referenced by:  relin1  4793  relin2  4794  reldif  4795  relres  4987  iss  5005  cnvdif  5089  funss  5290  funssres  5313  fliftcnv  5864  fliftfun  5865  reltpos  6336  tpostpos  6350  swoer  6648  erinxp  6696  ltrel  8134  lerel  8136  txdis1cn  14750  xmeter  14908  lgsquadlem1  15554  lgsquadlem2  15555