Theorem sseqtrrd 3918

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 2744	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 3917	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3843

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-in 3850  df-ss 3860

This theorem is referenced by:  sseqtrrid  3930  funfvima2d  7005  fnfvima  7006  wfrlem17  8000  oaordi  8203  omordi  8223  omlimcl  8235  oen0  8243  domunsncan  8666  f1opwfi  8901  cantnfle  9207  cantnflt  9208  cantnflem1d  9224  r1pwss  9286  rankxplim3  9383  acndom2  9554  fodomfi2  9560  cflm  9750  cflim2  9763  isf34lem5  9878  isf34lem7  9879  isf34lem6  9880  axdc2lem  9948  ttukeylem5  10013  wunex2  10238  ssfzunsn  13044  ccatass  14031  swrdval2  14097  splfv2a  14207  revccat  14217  cshimadifsn  14280  cshimadifsn0  14281  rtrclreclem1  14506  rtrclreclem2  14508  sumrblem  15161  prodrblem  15375  dfphi2  16211  vdwlem1  16417  basprssdmsets  16652  imasaddfnlem  16904  imasaddvallem  16905  imasvscafn  16913  imasvscaval  16914  mreexexlem4d  17021  mreexfidimd  17024  sscpwex  17190  acsmap2d  17905  gsumress  18008  subsubm  18097  frmdsssubm  18142  frmdss2  18144  subsubg  18420  cntzmhm2  18588  cntzcmnf  19084  ablcntzd  19096  gsumzsubmcl  19157  gsumconst  19173  gsumzmhm  19176  subgdmdprd  19275  dprdcntz2  19279  dprd2da  19283  dmdprdsplit2lem  19286  ablfac1eu  19314  pgpfaclem1  19322  pgpfaclem2  19323  issubdrg  19679  subsubrg  19680  subdrgint  19701  lmhmlsp  19940  lspsntri  19988  lspindpi  20023  lidldvgen  20147  gsumfsum  20284  mrccss  20510  frlmsslsp  20612  opsrtoslem2  20867  scmatsgrp1  21273  toponss  21678  ssntr  21809  elcls3  21834  toponmre  21844  neiptoptop  21882  neiptopnei  21883  neitr  21931  ordtbas  21943  ordtopn1  21945  ordtopn2  21946  iscnp3  21995  tgcn  22003  tgcnp  22004  ssidcn  22006  cnclsi  22023  cncls  22025  cncnp  22031  lmcld  22054  tgcmp  22152  cnconn  22173  connima  22176  clsconn  22181  conncompcld  22185  1stccnp  22213  kgentopon  22289  llycmpkgen2  22301  1stckgen  22305  kgencn2  22308  ptopn  22334  txcls  22355  ptpjcn  22362  ptclsg  22366  xkoccn  22370  txcnp  22371  ptcnplem  22372  txcmplem2  22393  xkoptsub  22405  xkopt  22406  xkoco2cn  22409  xkococnlem  22410  xkoinjcn  22438  imasnopn  22441  imasncld  22442  imasncls  22443  qtopkgen  22461  basqtop  22462  tgqtop  22463  qtoprest  22468  kqsat  22482  kqcldsat  22484  kqnrmlem1  22494  kqnrmlem2  22495  hmeontr  22520  reghmph  22544  nrmhmph  22545  fmfnfmlem4  22708  fmfnfm  22709  flimopn  22726  flimclslem  22735  flfnei  22742  lmflf  22756  txflf  22757  fclsopn  22765  fclsfnflim  22778  alexsublem  22795  ptcmplem3  22805  cnextcn  22818  efmndtmd  22852  submtmd  22855  subgtgp  22856  symgtgp  22857  clssubg  22860  clsnsg  22861  tgpconncompeqg  22863  snclseqg  22867  tsmscls  22889  trust  22981  restutop  22989  restutopopn  22990  utop3cls  23003  utopreg  23004  trcfilu  23046  blssec  23188  prdsbl  23244  blssopn  23248  metcnp  23294  cfilucfil  23312  psmetutop  23320  iccntr  23573  icccmplem2  23575  reconnlem1  23578  metnrmlem1a  23610  metnrmlem1  23611  metnrmlem2  23612  metnrmlem3  23613  cnheibor  23707  lebnumlem1  23713  lebnumlem3  23715  lebnumii  23718  clsocv  24002  iscfil2  24018  iscmet3  24045  cmetss  24068  relcmpcmet  24070  bcthlem5  24080  itg1addlem5  24453  perfdvf  24655  dvres3  24665  dvres3a  24666  dvcmul  24696  dvcmulf  24697  dvlip2  24747  lhop1lem  24765  dvcnvrelem1  24769  dvcnvrelem2  24770  dvcnvre  24771  dvcvx  24772  plyco0  24941  plyaddlem1  24962  plymullem1  24963  aalioulem3  25082  ulmdvlem1  25147  axcontlem10  26919  eengtrkg  26932  wlkp1lem7  27621  1wlkdlem4  28077  hsupunss  29278  pjpjpre  29354  ssmd2  30247  superpos  30289  atexch  30316  curry2ima  30616  pfxf1  30791  gsumhashmul  30893  symgcom2  30930  pmtrcnelor  30937  cycpmco2lem7  30976  cycpmconjvlem  30985  cycpmconjv  30986  cyc3conja  31001  nsgmgc  31169  nsgqusf1olem3  31172  elrspunidl  31178  mxidlprm  31212  lssdimle  31263  dimkerim  31280  fedgmullem1  31282  fedgmullem2  31283  fedgmul  31284  madjusmdetlem2  31350  zarclsun  31392  rhmpreimacnlem  31406  ordtconnlem1  31446  measiuns  31755  imambfm  31799  cnmbfm  31800  dya2iocnrect  31818  omsfval  31831  omssubaddlem  31836  omssubadd  31837  totprobd  31963  fzssfzo  32088  signstfvn  32118  bnj999  32509  bnj1408  32587  bnj1442  32600  bnj1450  32601  bnj1501  32618  fnrelpredd  32632  revwlk  32657  cvmsss2  32807  cvmliftmolem1  32814  cvmliftlem3  32820  cvmlift2lem9  32844  cvmlift2lem11  32846  cvmlift3lem6  32857  cvmlift3lem7  32858  ssmclslem  33098  mclsax  33102  mclsppslem  33116  mclspps  33117  dfrdg2  33343  trpredtr  33372  frrlem8  33448  frrlem10  33450  neiin  34159  neibastop2  34188  filnetlem4  34208  rdgssun  35172  lindsdom  35394  poimirlem11  35411  poimirlem12  35412  itg2addnclem2  35452  cnres2  35544  sstotbnd2  35555  sstotbnd  35556  prdstotbnd  35575  heibor1lem  35590  igenval2  35847  lshpnelb  36621  lcvexchlem4  36674  lsatexch  36680  l1cvat  36692  lkrscss  36735  lkrss  36805  lkreqN  36807  paddunN  37564  osumcllem2N  37594  pmapojoinN  37605  pl42lem2N  37617  dibglbN  38803  diblss  38807  dicvaddcl  38827  dicvscacl  38828  diclss  38830  cdlemn5pre  38837  dihord5apre  38899  dihglblem3N  38932  dihglb2  38979  dochsat  39020  dochshpncl  39021  djhspss  39043  dihsumssj  39045  mapdlsm  39301  hdmaprnlem3eN  39495  hdmaplkr  39550  fnwe2lem2  40448  lnmlsslnm  40478  lmhmfgima  40481  hbtlem6  40526  trrelsuperreldg  40822  iunrelexpuztr  40873  clsk1indlem2  41198  grumnudlem  41445  dvsconst  41486  dvsinax  42996  dvbdfbdioolem1  43011  itgsinexplem1  43037  itgperiod  43064  stoweidlem39  43122  dirkeritg  43185  fourierdlem48  43237  fourierdlem49  43238  fourierdlem70  43259  fourierdlem71  43260  fourierdlem81  43270  issalgend  43419  f1oresf1o  44315  subsubmgm  44885  rmsuppss  45240  restcls2lem  45728  iscnrm3rlem7  45762