Theorem relss 5638

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

Syntax hints:   → wi 4  Vcvv 3398   ⊆ wss 3853   × cxp 5534  Rel wrel 5541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-rel 5543

This theorem is referenced by:  relin1  5667  relin2  5668  reldif  5670  relres  5865  iss  5888  cnvdif  5987  difxp  6007  sofld  6030  funss  6377  funssres  6402  fliftcnv  7098  fliftfun  7099  releldmdifi  7794  frxp  7871  reltpos  7951  swoer  8399  sbthcl  8746  fpwwe2lem8  10217  recmulnq  10543  prcdnq  10572  ltrel  10860  lerel  10862  dfle2  12702  dflt2  12703  isinv  17219  invsym2  17222  invfun  17223  oppcsect2  17238  oppcinv  17239  relfull  17369  relfth  17370  psss  18040  gicer  18634  gsum2d  19311  isunit  19629  txdis1cn  22486  hmpher  22635  tgphaus  22968  qustgplem  22972  tsmsxp  23006  xmeter  23285  ovoliunlem1  24353  taylf  25207  lgsquadlem1  26215  lgsquadlem2  26216  nvrel  28637  phrel  28850  bnrel  28902  hlrel  28925  gonan0  33021  frxp2  33471  frxp3  33477  sscoid  33901  trer  34191  fneer  34228  heicant  35498  iss2  36165  funALTVss  36496  disjss  36528  dvhopellsm  38817  diclspsn  38894  dih1dimatlem  39029