Theorem sseqtrd 3986

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

Hypotheses

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

Assertion

Ref	Expression
sseqtrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrd

Step	Hyp	Ref	Expression
1		sseqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	sseq2d 3982	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶))
4	1, 3	mpbid 232	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  sseqtrrd  3987  sseqtrid  3992  3sstr3d  4004  uniintsn  4952  fssdmd  6709  oeeui  8569  nnaword2  8597  oaabs2  8616  naddword2  8659  erssxp  8697  fipwuni  9384  cantnflem3  9651  ficardun2  10162  ackbij1lem12  10190  ackbij1b  10198  fin1a2lem13  10372  winafp  10657  ioodisj  13450  reltrclfv  14990  prodss  15920  mrcssv  17582  mrcsscl  17588  mrcuni  17589  mressmrcd  17595  mreexexlem2d  17613  mreexexlem3d  17614  mreexfidimd  17618  subcss2  17812  resssetc  18061  funcsetcres2  18062  estrres  18107  poslubdg  18380  ipodrsfi  18505  acsmap2d  18521  mrelatlub  18528  mreclatBAD  18529  subsubmgm  18644  subsubm  18750  subsubg  19088  trivsubgd  19092  trivnsgd  19111  oppglsm  19579  subglsm  19610  lsmdisj  19618  gsumval3  19844  dprdres  19967  dprdss  19968  dprd2da  19981  dmdprdsplit2lem  19984  ablfac1b  20009  pgpfac1lem3  20016  subsubrng  20479  subsubrg  20514  rgspnval  20528  issubdrg  20696  islssd  20848  lspun  20900  lspssp  20901  lsslsp  20928  lsslspOLD  20929  lsmssspx  21002  lspabs2  21037  lspabs3  21038  lspsolvlem  21059  lbsextlem3  21077  qsssubdrg  21350  obselocv  21644  lsslindf  21746  sraassa  21785  mplbas2  21956  gsumply1subr  22125  tgcl  22863  basgen  22882  tgfiss  22885  bastop1  22887  bastop2  22888  clsss2  22966  elcls3  22977  topssnei  23018  neiptopnei  23026  neitr  23074  restcls  23075  restlp  23077  ordtrest2  23098  iscncl  23163  cncls2  23167  cncls  23168  cnntr  23169  lmcls  23196  tgcmp  23295  cmpcld  23296  uncmp  23297  hauscmplem  23300  cmpfi  23302  clsconn  23324  2ndcsb  23343  2ndcctbss  23349  2ndcomap  23352  nllyrest  23380  1stckgenlem  23447  kgencn2  23451  kgen2cn  23453  ptbasfi  23475  txcld  23497  txcls  23498  txbasval  23500  neitx  23501  ptcld  23507  ptclsg  23509  txnlly  23531  hausdiag  23539  txkgen  23546  xkopt  23549  xkopjcn  23550  xkococnlem  23553  cnmpt1res  23570  cnmpt2res  23571  imasnopn  23584  imasncld  23585  imasncls  23586  qtopcld  23607  qtoprest  23611  qtopcmap  23613  kqcldsat  23627  kqreglem2  23636  kqnrmlem2  23638  hmeontr  23663  neifil  23774  fgtr  23784  trnei  23786  uffixfr  23817  uffix2  23818  uffixsn  23819  elflim  23865  flimclslem  23878  fclsopn  23908  fclscmpi  23923  fclscmp  23924  alexsubALTlem3  23943  alexsubALT  23945  ptcmplem3  23948  subgntr  24001  opnsubg  24002  clssubg  24003  clsnsg  24004  cldsubg  24005  tgpconncompeqg  24006  snclseqg  24010  tsmsgsum  24033  tsmsid  24034  tgptsmscld  24045  ustssco  24109  utop2nei  24145  utop3cls  24146  utopreg  24147  cnextucn  24197  ressprdsds  24266  lpbl  24398  met2ndci  24417  prdsxmslem2  24424  metustexhalf  24451  psmetutop  24462  tgioo  24691  metdstri  24747  metdseq0  24750  xlebnum  24871  clsocv  25157  metelcls  25212  metsscmetcld  25222  cmetss  25223  relcmpcmet  25225  cmpcmet  25226  minveclem4a  25337  uniioovol  25487  uniioombllem3  25493  limcres  25794  dvbss  25809  perfdvf  25811  dvreslem  25817  dvres2lem  25818  dvmptresicc  25824  dvcnp2  25828  dvcnp2OLD  25829  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcmulf  25855  dvcj  25861  dvnfre  25863  dvmptres2  25873  dvmptcmul  25875  dvmptntr  25882  dvlip2  25907  dvcnvrelem2  25930  ftc1cn  25957  dvntaylp  26286  taylthlem1  26288  ulmdvlem3  26318  pserulm  26338  nodense  27611  mulsproplem13  28038  mulsproplem14  28039  shsub2  31261  spanssoc  31285  shub2  31319  ococin  31344  ssjo  31383  chub2  31444  spanpr  31516  elnlfn  31864  mdslj1i  32255  mdslmd3i  32268  mdexchi  32271  chirredlem1  32326  atcvat3i  32332  mdsymlem1  32339  mdsymlem5  32343  imadifxp  32537  fnpreimac  32602  suppovss  32611  symgcom2  33048  pmtrcnelor  33055  cycpmco2f1  33088  0ringsubrg  33209  erlval  33216  1fldgenq  33279  0ringidl  33399  elrspunidl  33406  0ringprmidl  33427  drngmxidl  33455  drngmxidlr  33456  idlsrgmulrss1  33489  idlsrgmulrss2  33490  1arithidomlem2  33514  ply1dg3rt0irred  33558  resssra  33590  lsssra  33591  drgextlsp  33596  lvecdim0  33609  lbslsat  33619  dimkerim  33630  fedgmullem2  33633  fedgmul  33634  fldgenfldext  33670  fldextrspunlsplem  33675  fldextrspunlsp  33676  fldextrspunlem1  33677  fldextrspunfld  33678  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  algextdeglem3  33716  algextdeglem4  33717  qtophaus  33833  locfinreflem  33837  rspecbas  33862  zarclssn  33870  zarmxt1  33877  zarcmplem  33878  fsumcvg4  33947  esum2d  34090  omsmon  34296  omssubadd  34298  carsgclctun  34319  sitgclg  34340  eulerpartlemgf  34377  reprpmtf1o  34624  cvmscld  35267  cvmliftmolem1  35275  cvmlift2lem9  35305  cvmlift2lem11  35307  cvmlift3lem6  35318  opnregcld  36325  ivthALT  36330  neibastop2  36356  fnemeet1  36361  fnejoin1  36363  pibt2  37412  poimirlem11  37632  poimirlem12  37633  poimirlem30  37651  ftc1cnnc  37693  sstotbnd  37776  ssbnd  37789  heibor1lem  37810  heiborlem3  37814  heibor  37822  lsmsat  39008  lssats  39012  lcvexchlem3  39036  lsatcvat3  39052  lkrscss  39098  lkrpssN  39163  pmod1i  39849  pclbtwnN  39898  pclunN  39899  pclss2polN  39922  pcl0N  39923  sspmaplubN  39926  paddunN  39928  pnonsingN  39934  pclfinclN  39951  osumcllem4N  39960  dia2dimlem13  41077  dvhopellsm  41118  dvadiaN  41129  dicelval1stN  41189  dicelval2nd  41190  dihssxp  41253  dihvalrel  41280  dochsscl  41369  dihoml4  41378  dochnoncon  41392  dvh3dim3N  41450  lcfrlem2  41544  lcfrlem5  41547  lcfr  41586  lcdlsp  41622  mapdsn  41642  mapdlsm  41665  mapdpglem1  41673  mapdindp0  41720  hlhilocv  41958  primrootscoprbij  42097  rntrclfvOAI  42686  ismrcd1  42693  ismrcd2  42694  coeq0i  42748  hbtlem6  43125  iocinico  43208  omabs2  43328  naddwordnexlem4  43397  trclubNEW  43615  ntrk2imkb  44033  isotone1  44044  k0004ss3  44149  iccdifprioo  45521  limsupequzmptlem  45733  cncfuni  45891  cncfiooicclem1  45898  dvresntr  45923  itgsubsticclem  45980  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  qndenserrn  46304  prsal  46323  intsaluni  46334  sssalgen  46340  dfsalgen2  46346  sge0split  46414  ismeannd  46472  caragensspw  46514  caragendifcl  46519  carageniuncl  46528  caratheodorylem1  46531  hoicvrrex  46561  ovnssle  46566  ovn02  46573  ovnsubadd  46577  hoidmv1le  46599  ovnlecvr2  46615  ovncvr2  46616  isvonmbl  46643  vonmblss  46645  ovolval4lem2  46655  ovnovollem1  46661  ovnovollem2  46662  incsmf  46747  decsmf  46772  uspgropssxp  48136  mreuniss  48892  restcls2lem  48905  restcls2  48906  cnneiima  48909  imassc  49146