Theorem relss 5759

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

This proof depends on syntax axioms:   → wi 4  Vcvv 3450   ⊆ wss 3896   × cxp 5649  Rel wrel 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ss 3897  df-rel 5658

This theorem is used by:  relin1  5791  relin2  5792  reldif  5794  relresOLD  5998  iss  6029  cnvdif  6136  difxp  6157  sofld  6181  funss  6563  funssres  6589  fliftcnv  7323  fliftfun  7324  releldmdifi  8061  frxp  8145  frxp2  8168  frxp3  8175  reltpos  8256  swoer  8757  sbthcl  9126  fpwwe2lem8  10730  recmulnq  11056  prcdnq  11085  ltrel  11378  lerel  11380  dfle2  13283  dflt2  13284  isinv  17944  invsym2  17947  invfun  17948  oppcsect2  17963  oppcinv  17964  relfull  18094  relfth  18095  psss  18763  gicer  19500  gsum2d  20195  isunit  20612  ricrel  20753  txdis1cn  23963  hmpher  24112  tgphaus  24445  qustgplem  24449  tsmsxp  24483  xmeter  24761  ovoliunlem1  25832  taylf  26697  lgsquadlem1  27716  lgsquadlem2  27717  noseqrdgfn  28701  nvrel  31213  phrel  31426  bnrel  31478  hlrel  31501  gsumfs2d  33672  elrgspnsubrunlem2  33859  gonan0  36275  sscoid  36799  trer  37228  fneer  37265  heicant  38710  iss2  39413  funALTVss  39853  disjss  39900  dvhopellsm  42311  diclspsn  42388  dih1dimatlem  42523  hfstructfun  46162  gricrel  49153  grlicrel  49240