Theorem relss 4921

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

Syntax hints:   -> wi 4   _Vcvv 3044   C_ wss 3403   X. cxp 4831   Rel wrel 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3410  df-ss 3417  df-rel 4840

This theorem is referenced by:  relin1  4950  relin2  4951  reldif  4952  relres  5131  iss  5151  cnvdif  5241  difxp  5260  sofld  5283  funss  5599  funssres  5621  fliftcnv  6202  fliftfun  6203  frxp  6903  reltpos  6975  tpostpos  6990  swoer  7388  erinxp  7434  sbthcl  7691  fpwwe2lem8  9059  fpwwe2lem9  9060  fpwwe2lem12  9063  recmulnq  9386  prcdnq  9415  ltrel  9693  lerel  9695  dfle2  11443  dflt2  11444  pwsle  15383  isinv  15658  invsym2  15661  invfun  15662  oppcsect2  15677  oppcinv  15678  relfull  15806  relfth  15807  psss  16453  gicer  16933  gsum2d  17597  isunit  17878  opsrtoslem2  18701  txdis1cn  20643  hmpher  20792  tgphaus  21124  qustgplem  21128  tsmsxp  21162  xmeter  21441  ovoliunlem1  22448  taylf  23309  lgsquadlem1  24275  lgsquadlem2  24276  nvrel  26214  phrel  26449  bnrel  26502  hlrel  26535  elrn3  30396  sscoid  30673  trer  30965  fneer  31002  heicant  31968  dvhopellsm  34679  diclspsn  34756  dih1dimatlem  34891