Theorem sseqtrrd 3959

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

Hypotheses

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

Assertion

Ref	Expression
sseqtrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrrd

Step	Hyp	Ref	Expression
1		sseqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2746	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 3958	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  3sstr4d  3977  fssrescdmd  7075  funfvima2d  7183  fnfvima  7184  frrlem8  8240  frrlem10  8242  fprresex  8257  oaordi  8478  omordi  8498  omlimcl  8510  oen0  8519  domunsncan  9012  f1opwfi  9263  cantnfle  9590  cantnflt  9591  cantnflem1d  9607  ttrcltr  9635  r1pwss  9706  rankxplim3  9803  acndom2  9974  fodomfi2  9980  cflm  10170  cflim2  10183  isf34lem5  10298  isf34lem7  10299  isf34lem6  10300  axdc2lem  10368  ttukeylem5  10433  wunex2  10659  ssfzunsn  13522  ccatass  14549  swrdval2  14607  splfv2a  14716  revccat  14726  cshimadifsn  14789  cshimadifsn0  14790  rtrclreclem1  15017  rtrclreclem2  15019  sumrblem  15671  prodrblem  15892  dfphi2  16742  vdwlem1  16950  basprssdmsets  17189  imasaddfnlem  17490  imasaddvallem  17491  imasvscafn  17499  imasvscaval  17500  mreexexlem4d  17611  mreexfidimd  17614  sscpwex  17780  acsmap2d  18519  gsumress  18648  subsubmgm  18676  subsubm  18782  frmdsssubm  18827  frmdss2  18829  subsubg  19123  cntzmhm2  19315  cntzcmnf  19818  ablcntzd  19830  gsumzsubmcl  19891  gsumconst  19907  gsumzmhm  19910  subgdmdprd  20009  dprdcntz2  20013  dprd2da  20017  dmdprdsplit2lem  20020  ablfac1eu  20048  pgpfaclem1  20056  pgpfaclem2  20057  subsubrng  20542  subsubrg  20577  issubdrg  20759  subdrgint  20782  lmhmlsp  21046  lspsntri  21094  lspindpi  21132  lidldvgen  21334  gsumfsum  21416  mrccss  21676  frlmsslsp  21778  opsrtoslem2  22039  ressply1evl  22363  scmatsgrp1  22512  toponss  22917  ssntr  23048  elcls3  23073  toponmre  23083  neiptoptop  23121  neiptopnei  23122  neitr  23170  ordtbas  23182  ordtopn1  23184  ordtopn2  23185  iscnp3  23234  tgcn  23242  tgcnp  23243  ssidcn  23245  cnclsi  23262  cncls  23264  cncnp  23270  lmcld  23293  tgcmp  23391  cnconn  23412  connima  23415  clsconn  23420  conncompcld  23424  1stccnp  23452  kgentopon  23528  llycmpkgen2  23540  1stckgen  23544  kgencn2  23547  ptopn  23573  txcls  23594  ptpjcn  23601  ptclsg  23605  xkoccn  23609  txcnp  23610  ptcnplem  23611  txcmplem2  23632  xkoptsub  23644  xkopt  23645  xkoco2cn  23648  xkococnlem  23649  xkoinjcn  23677  imasnopn  23680  imasncld  23681  imasncls  23682  qtopkgen  23700  basqtop  23701  tgqtop  23702  qtoprest  23707  kqsat  23721  kqcldsat  23723  kqnrmlem1  23733  kqnrmlem2  23734  hmeontr  23759  reghmph  23783  nrmhmph  23784  fmfnfmlem4  23947  fmfnfm  23948  flimopn  23965  flimclslem  23974  flfnei  23981  lmflf  23995  txflf  23996  fclsopn  24004  fclsfnflim  24017  alexsublem  24034  ptcmplem3  24044  cnextcn  24057  efmndtmd  24091  submtmd  24094  subgtgp  24095  symgtgp  24096  clssubg  24099  clsnsg  24100  tgpconncompeqg  24102  snclseqg  24106  tsmscls  24128  trust  24219  restutop  24227  restutopopn  24228  utop3cls  24241  utopreg  24242  trcfilu  24283  blssec  24425  prdsbl  24481  blssopn  24485  metcnp  24531  cfilucfil  24549  psmetutop  24557  iccntr  24812  icccmplem2  24814  reconnlem1  24817  metnrmlem1a  24849  metnrmlem1  24850  metnrmlem2  24851  metnrmlem3  24852  cnheibor  24947  lebnumlem1  24953  lebnumlem3  24955  lebnumii  24958  clsocv  25242  iscfil2  25258  iscmet3  25285  cmetss  25308  relcmpcmet  25310  bcthlem5  25320  itg1addlem5  25692  perfdvf  25895  dvres3  25905  dvres3a  25906  dvcmul  25936  dvcmulf  25937  dvlip2  25987  lhop1lem  26005  dvcnvrelem1  26009  dvcnvrelem2  26010  dvcnvre  26011  dvcvx  26012  plyco0  26182  plyaddlem1  26203  plymullem1  26204  aalioulem3  26325  ulmdvlem1  26390  precsexlem6  28229  precsexlem7  28230  bdayn0p1  28386  bdaypw2n0bndlem  28480  z12bdaylem2  28488  axcontlem10  29067  eengtrkg  29080  wlkp1lem7  29771  cyclnumvtx  29893  1wlkdlem4  30235  hsupunss  31439  pjpjpre  31515  ssmd2  32408  superpos  32450  atexch  32477  curry2ima  32808  pfxf1  33028  gsumhashmul  33155  symgcom2  33172  pmtrcnelor  33179  cycpmco2lem7  33220  cycpmconjvlem  33229  cycpmconjv  33230  cyc3conja  33245  elrgspnsubrunlem2  33336  subsdrg  33389  nsgmgc  33502  nsgqusf1olem3  33505  elrspunidl  33518  mxidlprm  33560  rprmdvdsprod  33624  dfufd2lem  33639  esplyfvaln  33765  lssdimle  33799  dimkerim  33818  fedgmullem1  33820  fedgmullem2  33821  fedgmul  33822  dimlssid  33823  fldsdrgfldext2  33853  fldextrspunlsplem  33864  fldextrspunlsp  33865  fldextrspunlem1  33866  fldextrspundgdvdslem  33871  fldextrspundgdvds  33872  constr01  33933  constrmon  33935  constrextdg2lem  33939  constrext2chnlem  33941  madjusmdetlem2  34019  zarclsun  34061  rhmpreimacnlem  34075  ordtconnlem1  34115  measiuns  34408  imambfm  34453  cnmbfm  34454  dya2iocnrect  34472  omsfval  34485  omssubaddlem  34490  omssubadd  34491  totprobd  34617  fzssfzo  34730  signstfvn  34760  bnj999  35147  bnj1408  35225  bnj1442  35238  bnj1450  35239  bnj1501  35256  fnrelpredd  35279  revwlk  35360  cvmsss2  35509  cvmliftmolem1  35516  cvmliftlem3  35522  cvmlift2lem9  35546  cvmlift2lem11  35548  cvmlift3lem6  35559  cvmlift3lem7  35560  ssmclslem  35800  mclsax  35804  mclsppslem  35818  mclspps  35819  dfrdg2  36028  neiin  36567  neibastop2  36596  filnetlem4  36616  weiunfrlem  36699  rdgssun  37747  lindsdom  37988  poimirlem11  38005  poimirlem12  38006  itg2addnclem2  38046  cnres2  38137  sstotbnd2  38148  sstotbnd  38149  prdstotbnd  38168  heibor1lem  38183  igenval2  38440  lshpnelb  39483  lcvexchlem4  39536  lsatexch  39542  l1cvat  39554  lkrscss  39597  lkrss  39667  lkreqN  39669  paddunN  40426  osumcllem2N  40456  pmapojoinN  40467  pl42lem2N  40479  dibglbN  41665  diblss  41669  dicvaddcl  41689  dicvscacl  41690  diclss  41692  cdlemn5pre  41699  dihord5apre  41761  dihglblem3N  41794  dihglb2  41841  dochsat  41882  dochshpncl  41883  djhspss  41905  dihsumssj  41907  mapdlsm  42163  hdmaprnlem3eN  42357  hdmaplkr  42412  fnwe2lem2  43503  lnmlsslnm  43533  lmhmfgima  43536  hbtlem6  43581  omabs2  43784  tfsconcatrev  43800  naddwordnexlem0  43848  trrelsuperreldg  44119  iunrelexpuztr  44170  clsk1indlem2  44493  grumnudlem  44736  dvsconst  44781  dvsinax  46363  dvbdfbdioolem1  46378  itgsinexplem1  46404  itgperiod  46431  stoweidlem39  46489  dirkeritg  46552  fourierdlem48  46604  fourierdlem49  46605  fourierdlem70  46626  fourierdlem71  46627  fourierdlem81  46637  issalgend  46788  chnsubseqwl  47331  f1oresf1o  47760  clnbgrgrim  48432  rmsuppss  48868  restcls2lem  49410  iscnrm3rlem7  49443