Theorem sseqtr4d 3866

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
sseqtr4d.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sseqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
sseqtr4d	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtr4d

Step	Hyp	Ref	Expression
1		sseqtr4d.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2830	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 3865	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1658   ⊆ wss 3797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-in 3804  df-ss 3811

This theorem is referenced by:  syl5sseqr  3878  fnfvima  6751  wfrlem17  7696  oaordi  7892  omordi  7912  omlimcl  7924  oen0  7932  domunsncan  8328  f1opwfi  8538  cantnfle  8844  cantnflt  8845  cantnflem1d  8861  r1pwss  8923  rankxplim3  9020  acndom2  9189  fodomfi2  9195  cflm  9386  cflim2  9399  isf34lem5  9514  isf34lem7  9515  isf34lem6  9516  axdc2lem  9584  ttukeylem5  9649  wunex2  9874  ssfzunsn  12679  ccatass  13647  swrdval2  13705  pfxccatin12  13830  swrdccatin12OLD  13831  splfv2a  13869  splfv2aOLD  13870  revccat  13881  cshimadifsn  13949  cshimadifsn0  13950  rtrclreclem1  14174  rtrclreclem2  14175  sumrblem  14818  prodrblem  15031  dfphi2  15849  vdwlem1  16055  basprssdmsets  16287  imasaddfnlem  16540  imasaddvallem  16541  imasvscafn  16549  imasvscaval  16550  mreexexlem4d  16659  mreexfidimd  16662  sscpwex  16826  acsmap2d  17531  gsumress  17628  subsubm  17709  frmdsssubm  17751  frmdss2  17753  subsubg  17967  cntzmhm2  18121  cntzcmnf  18600  ablcntzd  18612  gsumzsubmcl  18670  gsumconst  18686  gsumzmhm  18689  subgdmdprd  18786  dprdcntz2  18790  dprd2da  18794  dmdprdsplit2lem  18797  ablfac1eu  18825  pgpfaclem1  18833  pgpfaclem2  18834  issubdrg  19160  subsubrg  19161  lmhmlsp  19407  lspsntri  19455  lspindpi  19491  lidldvgen  19615  opsrtoslem2  19844  gsumfsum  20172  mrccss  20400  frlmsslsp  20501  scmatsgrp1  20695  toponss  21101  ssntr  21232  elcls3  21257  toponmre  21267  neiptoptop  21305  neiptopnei  21306  neitr  21354  ordtbas  21366  ordtopn1  21368  ordtopn2  21369  iscnp3  21418  tgcn  21426  tgcnp  21427  ssidcn  21429  cnclsi  21446  cncls  21448  cncnp  21454  lmcld  21477  tgcmp  21574  cnconn  21595  connima  21598  clsconn  21603  conncompcld  21607  1stccnp  21635  kgentopon  21711  llycmpkgen2  21723  1stckgen  21727  kgencn2  21730  ptopn  21756  txcls  21777  ptpjcn  21784  ptclsg  21788  xkoccn  21792  txcnp  21793  ptcnplem  21794  txcmplem2  21815  xkoptsub  21827  xkopt  21828  xkoco2cn  21831  xkococnlem  21832  xkoinjcn  21860  imasnopn  21863  imasncld  21864  imasncls  21865  qtopkgen  21883  basqtop  21884  tgqtop  21885  qtoprest  21890  kqsat  21904  kqcldsat  21906  kqnrmlem1  21916  kqnrmlem2  21917  hmeontr  21942  reghmph  21966  nrmhmph  21967  fmfnfmlem4  22130  fmfnfm  22131  flimopn  22148  flimclslem  22157  flfnei  22164  lmflf  22178  txflf  22179  fclsopn  22187  fclsfnflim  22200  alexsublem  22217  ptcmplem3  22227  cnextcn  22240  symgtgp  22274  submtmd  22277  subgtgp  22278  clssubg  22281  clsnsg  22282  tgpconncompeqg  22284  snclseqg  22288  tsmscls  22310  trust  22402  restutop  22410  restutopopn  22411  utop3cls  22424  utopreg  22425  trcfilu  22467  blssec  22609  prdsbl  22665  blssopn  22669  metcnp  22715  cfilucfil  22733  psmetutop  22741  iccntr  22993  icccmplem2  22995  reconnlem1  22998  metnrmlem1a  23030  metnrmlem1  23031  metnrmlem2  23032  metnrmlem3  23033  cnheibor  23123  lebnumlem1  23129  lebnumlem3  23131  lebnumii  23134  clsocv  23417  iscfil2  23433  iscmet3  23460  cmetss  23483  relcmpcmet  23485  bcthlem5  23495  itg1addlem5  23865  perfdvf  24065  dvres3  24075  dvres3a  24076  dvcmul  24105  dvcmulf  24106  dvlip2  24156  lhop1lem  24174  dvcnvrelem1  24178  dvcnvrelem2  24179  dvcnvre  24180  dvcvx  24181  plyco0  24346  plyaddlem1  24367  plymullem1  24368  aalioulem3  24487  ulmdvlem1  24552  axcontlem10  26271  eengtrkg  26284  wlkp1lem7  26979  1wlkdlem4  27515  hsupunss  28756  pjpjpre  28832  ssmd2  29725  superpos  29767  atexch  29794  curry2ima  30033  madjusmdetlem2  30438  ordtconnlem1  30514  measiuns  30824  imambfm  30868  cnmbfm  30869  dya2iocnrect  30887  omsfval  30900  omssubaddlem  30905  omssubadd  30906  totprobd  31033  fzssfzo  31158  signstfvn  31192  bnj999  31572  bnj1408  31649  bnj1442  31662  bnj1450  31663  bnj1501  31680  cvmsss2  31801  cvmliftmolem1  31808  cvmliftlem3  31814  cvmlift2lem9  31838  cvmlift2lem11  31840  cvmlift3lem6  31851  cvmlift3lem7  31852  ssmclslem  32007  mclsax  32011  mclsppslem  32025  mclspps  32026  dfrdg2  32238  trpredtr  32267  frrlem11  32330  neiin  32864  neibastop2  32893  filnetlem4  32913  lindsdom  33946  poimirlem11  33963  poimirlem12  33964  itg2addnclem2  34004  cnres2  34103  sstotbnd2  34114  sstotbnd  34115  prdstotbnd  34134  heibor1lem  34149  igenval2  34406  lshpnelb  35058  lcvexchlem4  35111  lsatexch  35117  l1cvat  35129  lkrscss  35172  lkrss  35242  lkreqN  35244  paddunN  36001  osumcllem2N  36031  pmapojoinN  36042  pl42lem2N  36054  dibglbN  37240  diblss  37244  dicvaddcl  37264  dicvscacl  37265  diclss  37267  cdlemn5pre  37274  dihord5apre  37336  dihglblem3N  37369  dihglb2  37416  dochsat  37457  dochshpncl  37458  djhspss  37480  dihsumssj  37482  mapdlsm  37738  hdmaprnlem3eN  37932  hdmaplkr  37987  fnwe2lem2  38463  lnmlsslnm  38493  lmhmfgima  38496  hbtlem6  38541  trrelsuperreldg  38800  iunrelexpuztr  38851  clsk1indlem2  39179  funfvima2d  39308  dvsconst  39368  fnfvimad  40259  dvsinax  40921  dvbdfbdioolem1  40937  itgsinexplem1  40963  itgperiod  40990  stoweidlem39  41049  dirkeritg  41112  fourierdlem48  41164  fourierdlem49  41165  fourierdlem70  41186  fourierdlem71  41187  fourierdlem81  41197  issalgend  41346  f1oresf1o  42192  f1oresf1o2  42193  subsubmgm  42643  rmsuppss  42997