Theorem sstr2 3945

Description: Transitivity of subclass relationship. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) Avoid axioms. (Revised by GG, 19-May-2025.)

Assertion

Ref	Expression
sstr2	⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Proof of Theorem sstr2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		imim1 84	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
2	1	al2imi 1845	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3		df-ss 3923	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3923	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		df-ss 3923	. . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	4, 5	imbi12i 353	. 2 ⊢ ((𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
7	2, 3, 6	3imtr4i 295	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Syntax hints:   → wi 4  ∀wal 1568   ∈ wcel 2143   ⊆ wss 3906

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

This theorem depends on definitions:  df-bi 210  df-ss 3923

This theorem is referenced by:  sstr  3946  sstri  3947  sseq1  3963  sseq2  3964  ssun3  4134  ssun4  4135  ssinss1OLD  4200  sspw  4574  triun  5234  trintss  5238  exss  5446  frss  5627  relss  5770  funss  6557  funimass2  6621  fss  6724  limsssuc  7847  oaordi  8532  oeworde  8580  nnaordi  8605  sbthlem2  9077  sbthlem3  9078  sbthlem6  9081  domunfican  9282  fiint  9287  fiss  9385  dffi3  9392  inf3lem1  9598  trcl  9698  tcss  9712  ac10ct  10019  ackbij2lem4  10225  cfslb  10251  cfslbn  10252  cfcoflem  10257  coftr  10258  fin23lem15  10319  fin23lem20  10322  fin23lem36  10333  isf32lem1  10338  axdc3lem2  10436  ttukeylem2  10495  wunex2  10724  tskcard  10767  clsslem  15023  mrcss  17673  isacs2  17710  lubss  18570  frmdss2  18923  lsmlub  19735  gsumle  20216  lsslss  21063  lspss  21086  ocv2ss  21804  ocvsscon  21806  lindsss  21955  lsslinds  21962  aspss  22007  mplcoe1  22169  mplcoe5  22172  mdetunilem9  22758  tgss  23106  tgcl  23107  tgss3  23124  clsss  23192  ntrss  23193  neiss  23247  ssnei2  23254  opnnei  23258  cnpnei  23402  cnpco  23405  cncls  23412  cnprest  23427  hauscmp  23545  1stcfb  23583  1stcelcls  23599  reftr  23652  txcnpi  23746  txcnp  23758  txtube  23778  qtoptop2  23837  fgcl  24016  filssufilg  24049  ufileu  24057  uffix  24059  elfm2  24086  fmfnfmlem1  24092  fmco  24099  fbflim2  24115  flffbas  24133  flftg  24134  cnpflf2  24138  alexsubALTlem4  24188  neibl  24639  metcnp3  24678  xlebnum  25105  lebnumii  25106  caubl  25448  caublcls  25449  bcthlem2  25465  bcthlem5  25468  ovolsslem  25624  volsuplem  25695  dyadmbllem  25739  ellimc3  26019  limciun  26034  cpnord  26075  precsexlem6  28386  precsexlem7  28387  ubthlem1  31203  occon3  31630  chsupval  31668  chsupcl  31673  chsupss  31675  spanss  31681  chsupval2  31743  stlei  32573  dmdbr5  32641  mdsl0  32643  chrelat2i  32698  chirredlem1  32723  mdsymlem5  32740  mdsymlem6  32741  gsumvsca1  33527  gsumvsca2  33528  omsmon  34669  cvmliftlem15  35771  ss2mcls  36041  mclsax  36042  clsint2  36821  fgmin  36862  filnetlem4  36873  limsucncmpi  36937  bj-restpw  37715  bj-0int  37724  rdgssun  38005  ptrecube  38252  heiborlem1  38443  heiborlem8  38450  refrelsredund4  39346  refrelredund4  39349  funALTVss  39414  pclssN  40649  dochexmidlem7  42221  incssnn0  43425  islssfg2  43781  hbtlem6  43839  hess  44489  psshepw  44497  clsf2  44835  mnuunid  44970  ismnushort  44994  sspwimpcf  45611  sspwimpcfVD  45612  dvmptfprod  46642  sprsymrelfo  48229  elbigo2  49315  subthinc  50204  setrec1lem2  50449  setrec1lem4  50451  setrec2mpt  50458