Theorem relss 5738

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

Syntax hints:   → wi 4  Vcvv 3429   ⊆ wss 3889   × cxp 5629  Rel wrel 5636

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

This theorem depends on definitions:  df-bi 207  df-ss 3906  df-rel 5638

This theorem is referenced by:  relin1  5768  relin2  5769  reldif  5771  relres  5970  iss  6000  cnvdif  6107  difxp  6128  sofld  6151  funss  6517  funssres  6542  fliftcnv  7266  fliftfun  7267  releldmdifi  7998  frxp  8076  frxp2  8094  frxp3  8101  reltpos  8181  swoer  8675  sbthcl  9037  fpwwe2lem8  10561  recmulnq  10887  prcdnq  10916  ltrel  11207  lerel  11209  dfle2  13098  dflt2  13099  isinv  17727  invsym2  17730  invfun  17731  oppcsect2  17746  oppcinv  17747  relfull  17877  relfth  17878  psss  18546  gicer  19252  gsum2d  19947  isunit  20353  txdis1cn  23600  hmpher  23749  tgphaus  24082  qustgplem  24086  tsmsxp  24120  xmeter  24398  ovoliunlem1  25469  taylf  26326  lgsquadlem1  27343  lgsquadlem2  27344  noseqrdgfn  28298  nvrel  30673  phrel  30886  bnrel  30938  hlrel  30961  gsumfs2d  33122  elrgspnsubrunlem2  33309  gonan0  35574  sscoid  36093  trer  36498  fneer  36535  heicant  37976  iss2  38665  funALTVss  39105  disjss  39152  dvhopellsm  41563  diclspsn  41640  dih1dimatlem  41775  gricrel  48395  grlicrel  48482