Theorem relss 5744

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 3953	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V)))
2		df-rel 5645	. 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
3		df-rel 5645	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
4	1, 2, 3	3imtr4g 296	1 ⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴))

Syntax hints:   → wi 4  Vcvv 3447   ⊆ wss 3914   × cxp 5636  Rel wrel 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-ss 3931  df-rel 5645

This theorem is referenced by:  relin1  5775  relin2  5776  reldif  5778  relres  5976  iss  6006  cnvdif  6116  difxp  6137  sofld  6160  funss  6535  funssres  6560  fliftcnv  7286  fliftfun  7287  releldmdifi  8024  frxp  8105  frxp2  8123  frxp3  8130  reltpos  8210  swoer  8702  sbthcl  9063  fpwwe2lem8  10591  recmulnq  10917  prcdnq  10946  ltrel  11236  lerel  11238  dfle2  13107  dflt2  13108  isinv  17722  invsym2  17725  invfun  17726  oppcsect2  17741  oppcinv  17742  relfull  17872  relfth  17873  psss  18539  gicer  19209  gsum2d  19902  isunit  20282  txdis1cn  23522  hmpher  23671  tgphaus  24004  qustgplem  24008  tsmsxp  24042  xmeter  24321  ovoliunlem1  25403  taylf  26268  lgsquadlem1  27291  lgsquadlem2  27292  noseqrdgfn  28200  nvrel  30531  phrel  30744  bnrel  30796  hlrel  30819  gsumfs2d  32995  elrgspnsubrunlem2  33199  gonan0  35379  sscoid  35901  trer  36304  fneer  36341  heicant  37649  iss2  38326  funALTVss  38691  disjss  38723  dvhopellsm  41111  diclspsn  41188  dih1dimatlem  41323  gricrel  47919  grlicrel  47998