Theorem sseqtr4d 3642

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

Syntax hints:   → wi 4   = wceq 1483   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  syl5sseqr  3654  fnfvima  6496  wfrlem17  7431  oaordi  7626  omordi  7646  omlimcl  7658  oen0  7666  domunsncan  8060  f1opwfi  8270  cantnfle  8568  cantnflt  8569  cantnflem1d  8585  r1pwss  8647  rankxplim3  8744  acndom2  8877  fodomfi2  8883  cflm  9072  cflim2  9085  isf34lem5  9200  isf34lem7  9201  isf34lem6  9202  axdc2lem  9270  ttukeylem5  9335  wunex2  9560  ssfzunsn  12387  ccatass  13371  swrdval2  13420  swrdccatin12  13491  splfv2a  13507  revccat  13515  cshimadifsn  13575  cshimadifsn0  13576  rtrclreclem1  13798  rtrclreclem2  13799  sumrblem  14442  prodrblem  14659  dfphi2  15479  vdwlem1  15685  basprssdmsets  15925  imasaddfnlem  16188  imasaddvallem  16189  imasvscafn  16197  imasvscaval  16198  mreexexlem4d  16307  mreexfidimd  16311  sscpwex  16475  acsmap2d  17179  gsumress  17276  subsubm  17357  frmdsssubm  17398  frmdss2  17400  subsubg  17617  cntzmhm2  17772  cntzcmnf  18248  ablcntzd  18260  gsumzsubmcl  18318  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  subgdmdprd  18433  dprdcntz2  18437  dprd2da  18441  dmdprdsplit2lem  18444  ablfac1eu  18472  pgpfaclem1  18480  pgpfaclem2  18481  issubdrg  18805  subsubrg  18806  lmhmlsp  19049  lspsntri  19097  lspindpi  19132  lidldvgen  19255  opsrtoslem2  19485  gsumfsum  19813  mrccss  20038  frlmsslsp  20135  scmatsgrp1  20328  toponss  20731  ssntr  20862  elcls3  20887  toponmre  20897  neiptoptop  20935  neiptopnei  20936  neitr  20984  ordtbas  20996  ordtopn1  20998  ordtopn2  20999  iscnp3  21048  tgcn  21056  tgcnp  21057  ssidcn  21059  cnclsi  21076  cncls  21078  cncnp  21084  lmcld  21107  tgcmp  21204  cnconn  21225  connima  21228  clsconn  21233  conncompcld  21237  1stccnp  21265  kgentopon  21341  llycmpkgen2  21353  1stckgen  21357  kgencn2  21360  ptopn  21386  txcls  21407  ptpjcn  21414  ptclsg  21418  xkoccn  21422  txcnp  21423  ptcnplem  21424  txcmplem2  21445  xkoptsub  21457  xkopt  21458  xkoco2cn  21461  xkococnlem  21462  xkoinjcn  21490  imasnopn  21493  imasncld  21494  imasncls  21495  qtopkgen  21513  basqtop  21514  tgqtop  21515  qtoprest  21520  kqsat  21534  kqcldsat  21536  kqnrmlem1  21546  kqnrmlem2  21547  hmeontr  21572  reghmph  21596  nrmhmph  21597  fmfnfmlem4  21761  fmfnfm  21762  flimopn  21779  flimclslem  21788  flfnei  21795  lmflf  21809  txflf  21810  fclsopn  21818  fclsfnflim  21831  alexsublem  21848  ptcmplem3  21858  cnextcn  21871  symgtgp  21905  submtmd  21908  subgtgp  21909  clssubg  21912  clsnsg  21913  tgpconncompeqg  21915  snclseqg  21919  tsmscls  21941  trust  22033  restutop  22041  restutopopn  22042  utop3cls  22055  utopreg  22056  trcfilu  22098  blssec  22240  prdsbl  22296  blssopn  22300  metcnp  22346  cfilucfil  22364  psmetutop  22372  iccntr  22624  icccmplem2  22626  reconnlem1  22629  metnrmlem1a  22661  metnrmlem1  22662  metnrmlem2  22663  metnrmlem3  22664  cnheibor  22754  lebnumlem1  22760  lebnumlem3  22762  lebnumii  22765  clsocv  23049  iscfil2  23064  iscmet3  23091  cmetss  23113  relcmpcmet  23115  bcthlem5  23125  itg1addlem5  23467  perfdvf  23667  dvres3  23677  dvres3a  23678  dvcmul  23707  dvcmulf  23708  dvlip2  23758  lhop1lem  23776  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcnvre  23782  dvcvx  23783  plyco0  23948  plyaddlem1  23969  plymullem1  23970  aalioulem3  24089  ulmdvlem1  24154  axcontlem10  25853  eengtrkg  25865  nbupgruvtxres  26308  wlkp1lem7  26576  1wlkdlem4  27000  hsupunss  28202  pjpjpre  28278  ssmd2  29171  superpos  29213  atexch  29240  curry2ima  29486  madjusmdetlem2  29894  ordtconnlem1  29970  measiuns  30280  imambfm  30324  cnmbfm  30325  dya2iocnrect  30343  omsfval  30356  omssubaddlem  30361  omssubadd  30362  totprobd  30488  fzssfzo  30613  signstfvn  30646  bnj999  31027  bnj1408  31104  bnj1442  31117  bnj1450  31118  bnj1501  31135  cvmsss2  31256  cvmliftmolem1  31263  cvmliftlem3  31269  cvmlift2lem9  31293  cvmlift2lem11  31295  cvmlift3lem6  31306  cvmlift3lem7  31307  ssmclslem  31462  mclsax  31466  mclsppslem  31480  mclspps  31481  dfrdg2  31701  trpredtr  31730  neiin  32327  neibastop2  32356  filnetlem4  32376  lindsdom  33403  poimirlem11  33420  poimirlem12  33421  itg2addnclem2  33462  cnres2  33562  sstotbnd2  33573  sstotbnd  33574  prdstotbnd  33593  heibor1lem  33608  igenval2  33865  lshpnelb  34271  lcvexchlem4  34324  lsatexch  34330  l1cvat  34342  lkrscss  34385  lkrss  34455  lkreqN  34457  paddunN  35213  osumcllem2N  35243  pmapojoinN  35254  pl42lem2N  35266  dibglbN  36455  diblss  36459  dicvaddcl  36479  dicvscacl  36480  diclss  36482  cdlemn5pre  36489  dihord5apre  36551  dihglblem3N  36584  dihglb2  36631  dochsat  36672  dochshpncl  36673  djhspss  36695  dihsumssj  36697  mapdlsm  36953  hdmaprnlem3eN  37150  hdmaplkr  37205  fnwe2lem2  37621  lnmlsslnm  37651  lmhmfgima  37654  hbtlem6  37699  trrelsuperreldg  37960  iunrelexpuztr  38011  clsk1indlem2  38340  funfvima2d  38469  dvsconst  38529  fnfvimad  39459  dvsinax  40127  dvbdfbdioolem1  40143  itgsinexplem1  40169  itgperiod  40197  stoweidlem39  40256  dirkeritg  40319  fourierdlem48  40371  fourierdlem49  40372  fourierdlem70  40393  fourierdlem71  40394  fourierdlem81  40404  issalgend  40556  pfxccatin12  41425  subsubmgm  41797  rmsuppss  42151