Theorem relss 5682

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

Syntax hints:   → wi 4  Vcvv 3422   ⊆ wss 3883   × cxp 5578  Rel wrel 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-rel 5587

This theorem is referenced by:  relin1  5711  relin2  5712  reldif  5714  relres  5909  iss  5932  cnvdif  6036  difxp  6056  sofld  6079  funss  6437  funssres  6462  fliftcnv  7162  fliftfun  7163  releldmdifi  7859  frxp  7938  reltpos  8018  swoer  8486  sbthcl  8835  fpwwe2lem8  10325  recmulnq  10651  prcdnq  10680  ltrel  10968  lerel  10970  dfle2  12810  dflt2  12811  isinv  17389  invsym2  17392  invfun  17393  oppcsect2  17408  oppcinv  17409  relfull  17540  relfth  17541  psss  18213  gicer  18807  gsum2d  19488  isunit  19814  txdis1cn  22694  hmpher  22843  tgphaus  23176  qustgplem  23180  tsmsxp  23214  xmeter  23494  ovoliunlem1  24571  taylf  25425  lgsquadlem1  26433  lgsquadlem2  26434  nvrel  28865  phrel  29078  bnrel  29130  hlrel  29153  gonan0  33254  frxp2  33718  frxp3  33724  sscoid  34142  trer  34432  fneer  34469  heicant  35739  iss2  36406  funALTVss  36737  disjss  36769  dvhopellsm  39058  diclspsn  39135  dih1dimatlem  39270