Theorem relss 5129

Description: Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)

Assertion

Ref	Expression
relss	⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴))

Proof of Theorem relss

Step	Hyp	Ref	Expression
1		sstr2 3575	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V)))
2		df-rel 5045	. 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
3		df-rel 5045	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
4	1, 2, 3	3imtr4g 284	1 ⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴))

Syntax hints:   → wi 4  Vcvv 3173   ⊆ wss 3540   × cxp 5036  Rel wrel 5043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-rel 5045

This theorem is referenced by:  relin1  5159  relin2  5160  reldif  5161  relres  5346  iss  5367  cnvdif  5458  difxp  5477  sofld  5500  funss  5822  funssres  5844  fliftcnv  6461  fliftfun  6462  frxp  7174  reltpos  7244  tpostpos  7259  swoer  7659  erinxp  7708  sbthcl  7967  fpwwe2lem8  9338  fpwwe2lem9  9339  fpwwe2lem12  9342  recmulnq  9665  prcdnq  9694  ltrel  9979  lerel  9981  dfle2  11856  dflt2  11857  pwsle  15975  isinv  16243  invsym2  16246  invfun  16247  oppcsect2  16262  oppcinv  16263  relfull  16391  relfth  16392  psss  17037  gicer  17541  gicerOLD  17542  gsum2d  18194  isunit  18480  opsrtoslem2  19306  txdis1cn  21248  hmpher  21397  tgphaus  21730  qustgplem  21734  tsmsxp  21768  xmeter  22048  ovoliunlem1  23077  taylf  23919  lgsquadlem1  24905  lgsquadlem2  24906  nvrel  26841  phrel  27054  bnrel  27107  hlrel  27130  elrn3  30906  sscoid  31190  trer  31480  fneer  31518  heicant  32614  dvhopellsm  35424  diclspsn  35501  dih1dimatlem  35636