Theorem sseqtrd 3995

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 3991	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶))
4	1, 3	mpbid 232	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  sseqtrrd  3996  sseqtrid  4001  3sstr3d  4013  uniintsn  4961  fssdmd  6724  oeeui  8614  nnaword2  8642  oaabs2  8661  naddword2  8704  erssxp  8742  fipwuni  9438  cantnflem3  9705  ficardun2  10216  ackbij1lem12  10244  ackbij1b  10252  fin1a2lem13  10426  winafp  10711  ioodisj  13499  reltrclfv  15036  prodss  15963  mrcssv  17626  mrcsscl  17632  mrcuni  17633  mressmrcd  17639  mreexexlem2d  17657  mreexexlem3d  17658  mreexfidimd  17662  subcss2  17856  resssetc  18105  funcsetcres2  18106  estrres  18151  poslubdg  18424  ipodrsfi  18549  acsmap2d  18565  mrelatlub  18572  mreclatBAD  18573  subsubmgm  18688  subsubm  18794  subsubg  19132  trivsubgd  19136  trivnsgd  19155  oppglsm  19623  subglsm  19654  lsmdisj  19662  gsumval3  19888  dprdres  20011  dprdss  20012  dprd2da  20025  dmdprdsplit2lem  20028  ablfac1b  20053  pgpfac1lem3  20060  subsubrng  20523  subsubrg  20558  rgspnval  20572  issubdrg  20740  islssd  20892  lspun  20944  lspssp  20945  lsslsp  20972  lsslspOLD  20973  lsmssspx  21046  lspabs2  21081  lspabs3  21082  lspsolvlem  21103  lbsextlem3  21121  qsssubdrg  21394  obselocv  21688  lsslindf  21790  sraassa  21829  mplbas2  22000  gsumply1subr  22169  tgcl  22907  basgen  22926  tgfiss  22929  bastop1  22931  bastop2  22932  clsss2  23010  elcls3  23021  topssnei  23062  neiptopnei  23070  neitr  23118  restcls  23119  restlp  23121  ordtrest2  23142  iscncl  23207  cncls2  23211  cncls  23212  cnntr  23213  lmcls  23240  tgcmp  23339  cmpcld  23340  uncmp  23341  hauscmplem  23344  cmpfi  23346  clsconn  23368  2ndcsb  23387  2ndcctbss  23393  2ndcomap  23396  nllyrest  23424  1stckgenlem  23491  kgencn2  23495  kgen2cn  23497  ptbasfi  23519  txcld  23541  txcls  23542  txbasval  23544  neitx  23545  ptcld  23551  ptclsg  23553  txnlly  23575  hausdiag  23583  txkgen  23590  xkopt  23593  xkopjcn  23594  xkococnlem  23597  cnmpt1res  23614  cnmpt2res  23615  imasnopn  23628  imasncld  23629  imasncls  23630  qtopcld  23651  qtoprest  23655  qtopcmap  23657  kqcldsat  23671  kqreglem2  23680  kqnrmlem2  23682  hmeontr  23707  neifil  23818  fgtr  23828  trnei  23830  uffixfr  23861  uffix2  23862  uffixsn  23863  elflim  23909  flimclslem  23922  fclsopn  23952  fclscmpi  23967  fclscmp  23968  alexsubALTlem3  23987  alexsubALT  23989  ptcmplem3  23992  subgntr  24045  opnsubg  24046  clssubg  24047  clsnsg  24048  cldsubg  24049  tgpconncompeqg  24050  snclseqg  24054  tsmsgsum  24077  tsmsid  24078  tgptsmscld  24089  ustssco  24153  utop2nei  24189  utop3cls  24190  utopreg  24191  cnextucn  24241  ressprdsds  24310  lpbl  24442  met2ndci  24461  prdsxmslem2  24468  metustexhalf  24495  psmetutop  24506  tgioo  24735  metdstri  24791  metdseq0  24794  xlebnum  24915  clsocv  25202  metelcls  25257  metsscmetcld  25267  cmetss  25268  relcmpcmet  25270  cmpcmet  25271  minveclem4a  25382  uniioovol  25532  uniioombllem3  25538  limcres  25839  dvbss  25854  perfdvf  25856  dvreslem  25862  dvres2lem  25863  dvmptresicc  25869  dvcnp2  25873  dvcnp2OLD  25874  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  dvcmulf  25900  dvcj  25906  dvnfre  25908  dvmptres2  25918  dvmptcmul  25920  dvmptntr  25927  dvlip2  25952  dvcnvrelem2  25975  ftc1cn  26002  dvntaylp  26331  taylthlem1  26333  ulmdvlem3  26363  pserulm  26383  nodense  27656  mulsproplem13  28083  mulsproplem14  28084  shsub2  31306  spanssoc  31330  shub2  31364  ococin  31389  ssjo  31428  chub2  31489  spanpr  31561  elnlfn  31909  mdslj1i  32300  mdslmd3i  32313  mdexchi  32316  chirredlem1  32371  atcvat3i  32377  mdsymlem1  32384  mdsymlem5  32388  imadifxp  32582  fnpreimac  32649  suppovss  32658  symgcom2  33095  pmtrcnelor  33102  cycpmco2f1  33135  0ringsubrg  33246  erlval  33253  1fldgenq  33316  0ringidl  33436  elrspunidl  33443  0ringprmidl  33464  drngmxidl  33492  drngmxidlr  33493  idlsrgmulrss1  33526  idlsrgmulrss2  33527  1arithidomlem2  33551  ply1dg3rt0irred  33595  resssra  33627  lsssra  33628  drgextlsp  33633  lvecdim0  33646  lbslsat  33656  dimkerim  33667  fedgmullem2  33670  fedgmul  33671  fldgenfldext  33709  fldextrspunlsplem  33714  fldextrspunlsp  33715  fldextrspunlem1  33716  fldextrspunfld  33717  fldextrspundgdvdslem  33721  fldextrspundgdvds  33722  algextdeglem3  33753  algextdeglem4  33754  qtophaus  33867  locfinreflem  33871  rspecbas  33896  zarclssn  33904  zarmxt1  33911  zarcmplem  33912  fsumcvg4  33981  esum2d  34124  omsmon  34330  omssubadd  34332  carsgclctun  34353  sitgclg  34374  eulerpartlemgf  34411  reprpmtf1o  34658  cvmscld  35295  cvmliftmolem1  35303  cvmlift2lem9  35333  cvmlift2lem11  35335  cvmlift3lem6  35346  opnregcld  36348  ivthALT  36353  neibastop2  36379  fnemeet1  36384  fnejoin1  36386  pibt2  37435  poimirlem11  37655  poimirlem12  37656  poimirlem30  37674  ftc1cnnc  37716  sstotbnd  37799  ssbnd  37812  heibor1lem  37833  heiborlem3  37837  heibor  37845  lsmsat  39026  lssats  39030  lcvexchlem3  39054  lsatcvat3  39070  lkrscss  39116  lkrpssN  39181  pmod1i  39867  pclbtwnN  39916  pclunN  39917  pclss2polN  39940  pcl0N  39941  sspmaplubN  39944  paddunN  39946  pnonsingN  39952  pclfinclN  39969  osumcllem4N  39978  dia2dimlem13  41095  dvhopellsm  41136  dvadiaN  41147  dicelval1stN  41207  dicelval2nd  41208  dihssxp  41271  dihvalrel  41298  dochsscl  41387  dihoml4  41396  dochnoncon  41410  dvh3dim3N  41468  lcfrlem2  41562  lcfrlem5  41565  lcfr  41604  lcdlsp  41640  mapdsn  41660  mapdlsm  41683  mapdpglem1  41691  mapdindp0  41738  hlhilocv  41976  primrootscoprbij  42115  rntrclfvOAI  42714  ismrcd1  42721  ismrcd2  42722  coeq0i  42776  hbtlem6  43153  iocinico  43236  omabs2  43356  naddwordnexlem4  43425  trclubNEW  43643  ntrk2imkb  44061  isotone1  44072  k0004ss3  44177  iccdifprioo  45545  limsupequzmptlem  45757  cncfuni  45915  cncfiooicclem1  45922  dvresntr  45947  itgsubsticclem  46004  fourierdlem42  46178  fourierdlem48  46183  fourierdlem49  46184  fourierdlem50  46185  qndenserrn  46328  prsal  46347  intsaluni  46358  sssalgen  46364  dfsalgen2  46370  sge0split  46438  ismeannd  46496  caragensspw  46538  caragendifcl  46543  carageniuncl  46552  caratheodorylem1  46555  hoicvrrex  46585  ovnssle  46590  ovn02  46597  ovnsubadd  46601  hoidmv1le  46623  ovnlecvr2  46639  ovncvr2  46640  isvonmbl  46667  vonmblss  46669  ovolval4lem2  46679  ovnovollem1  46685  ovnovollem2  46686  incsmf  46771  decsmf  46796  uspgropssxp  48119  mreuniss  48874  restcls2lem  48887  restcls2  48888  cnneiima  48891  imassc  49093