Theorem sseqtrd 4035

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  sseqtrrd  4036  sseqtrid  4047  uniintsn  4989  fssdmd  6754  oeeui  8638  nnaword2  8666  oaabs2  8685  naddword2  8728  erssxp  8766  fipwuni  9463  cantnflem3  9728  ficardun2  10239  ackbij1lem12  10267  ackbij1b  10275  fin1a2lem13  10449  winafp  10734  ioodisj  13518  reltrclfv  15052  prodss  15979  mrcssv  17658  mrcsscl  17664  mrcuni  17665  mressmrcd  17671  mreexexlem2d  17689  mreexexlem3d  17690  mreexfidimd  17694  subcss2  17893  resssetc  18145  funcsetcres2  18146  estrres  18194  poslubdg  18471  ipodrsfi  18596  acsmap2d  18612  mrelatlub  18619  mreclatBAD  18620  subsubmgm  18735  subsubm  18841  subsubg  19179  trivsubgd  19183  trivnsgd  19202  oppglsm  19674  subglsm  19705  lsmdisj  19713  gsumval3  19939  dprdres  20062  dprdss  20063  dprd2da  20076  dmdprdsplit2lem  20079  ablfac1b  20104  pgpfac1lem3  20111  subsubrng  20579  subsubrg  20614  rgspnval  20628  issubdrg  20797  islssd  20950  lspun  21002  lspssp  21003  lsslsp  21030  lsslspOLD  21031  lsmssspx  21104  lspabs2  21139  lspabs3  21140  lspsolvlem  21161  lbsextlem3  21179  qsssubdrg  21461  obselocv  21765  lsslindf  21867  sraassa  21906  mplbas2  22077  gsumply1subr  22250  tgcl  22991  basgen  23010  tgfiss  23013  bastop1  23015  bastop2  23016  clsss2  23095  elcls3  23106  topssnei  23147  neiptopnei  23155  neitr  23203  restcls  23204  restlp  23206  ordtrest2  23227  iscncl  23292  cncls2  23296  cncls  23297  cnntr  23298  lmcls  23325  tgcmp  23424  cmpcld  23425  uncmp  23426  hauscmplem  23429  cmpfi  23431  clsconn  23453  2ndcsb  23472  2ndcctbss  23478  2ndcomap  23481  nllyrest  23509  1stckgenlem  23576  kgencn2  23580  kgen2cn  23582  ptbasfi  23604  txcld  23626  txcls  23627  txbasval  23629  neitx  23630  ptcld  23636  ptclsg  23638  txnlly  23660  hausdiag  23668  txkgen  23675  xkopt  23678  xkopjcn  23679  xkococnlem  23682  cnmpt1res  23699  cnmpt2res  23700  imasnopn  23713  imasncld  23714  imasncls  23715  qtopcld  23736  qtoprest  23740  qtopcmap  23742  kqcldsat  23756  kqreglem2  23765  kqnrmlem2  23767  hmeontr  23792  neifil  23903  fgtr  23913  trnei  23915  uffixfr  23946  uffix2  23947  uffixsn  23948  elflim  23994  flimclslem  24007  fclsopn  24037  fclscmpi  24052  fclscmp  24053  alexsubALTlem3  24072  alexsubALT  24074  ptcmplem3  24077  subgntr  24130  opnsubg  24131  clssubg  24132  clsnsg  24133  cldsubg  24134  tgpconncompeqg  24135  snclseqg  24139  tsmsgsum  24162  tsmsid  24163  tgptsmscld  24174  ustssco  24238  utop2nei  24274  utop3cls  24275  utopreg  24276  cnextucn  24327  ressprdsds  24396  lpbl  24531  met2ndci  24550  prdsxmslem2  24557  metustexhalf  24584  psmetutop  24595  tgioo  24831  metdstri  24886  metdseq0  24889  xlebnum  25010  clsocv  25297  metelcls  25352  metsscmetcld  25362  cmetss  25363  relcmpcmet  25365  cmpcmet  25366  minveclem4a  25477  uniioovol  25627  uniioombllem3  25633  limcres  25935  dvbss  25950  perfdvf  25952  dvreslem  25958  dvres2lem  25959  dvmptresicc  25965  dvcnp2  25969  dvcnp2OLD  25970  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcmulf  25996  dvcj  26002  dvnfre  26004  dvmptres2  26014  dvmptcmul  26016  dvmptntr  26023  dvlip2  26048  dvcnvrelem2  26071  ftc1cn  26098  dvntaylp  26427  taylthlem1  26429  ulmdvlem3  26459  pserulm  26479  nodense  27751  mulsproplem13  28168  mulsproplem14  28169  shsub2  31353  spanssoc  31377  shub2  31411  ococin  31436  ssjo  31475  chub2  31536  spanpr  31608  elnlfn  31956  mdslj1i  32347  mdslmd3i  32360  mdexchi  32363  chirredlem1  32418  atcvat3i  32424  mdsymlem1  32431  mdsymlem5  32435  imadifxp  32620  fnpreimac  32687  suppovss  32695  symgcom2  33086  pmtrcnelor  33093  cycpmco2f1  33126  0ringsubrg  33237  erlval  33244  1fldgenq  33303  0ringidl  33428  elrspunidl  33435  0ringprmidl  33456  drngmxidl  33484  drngmxidlr  33485  idlsrgmulrss1  33518  idlsrgmulrss2  33519  1arithidomlem2  33543  ply1dg3rt0irred  33586  resssra  33616  lsssra  33617  drgextlsp  33622  lvecdim0  33633  lbslsat  33643  dimkerim  33654  fedgmullem2  33657  fedgmul  33658  fldgenfldext  33692  algextdeglem3  33724  algextdeglem4  33725  qtophaus  33796  locfinreflem  33800  rspecbas  33825  zarclssn  33833  zarmxt1  33840  zarcmplem  33841  fsumcvg4  33910  esum2d  34073  omsmon  34279  omssubadd  34281  carsgclctun  34302  sitgclg  34323  eulerpartlemgf  34360  reprpmtf1o  34619  cvmscld  35257  cvmliftmolem1  35265  cvmlift2lem9  35295  cvmlift2lem11  35297  cvmlift3lem6  35308  opnregcld  36312  ivthALT  36317  neibastop2  36343  fnemeet1  36348  fnejoin1  36350  pibt2  37399  poimirlem11  37617  poimirlem12  37618  poimirlem30  37636  ftc1cnnc  37678  sstotbnd  37761  ssbnd  37774  heibor1lem  37795  heiborlem3  37799  heibor  37807  lsmsat  38989  lssats  38993  lcvexchlem3  39017  lsatcvat3  39033  lkrscss  39079  lkrpssN  39144  pmod1i  39830  pclbtwnN  39879  pclunN  39880  pclss2polN  39903  pcl0N  39904  sspmaplubN  39907  paddunN  39909  pnonsingN  39915  pclfinclN  39932  osumcllem4N  39941  dia2dimlem13  41058  dvhopellsm  41099  dvadiaN  41110  dicelval1stN  41170  dicelval2nd  41171  dihssxp  41234  dihvalrel  41261  dochsscl  41350  dihoml4  41359  dochnoncon  41373  dvh3dim3N  41431  lcfrlem2  41525  lcfrlem5  41528  lcfr  41567  lcdlsp  41603  mapdsn  41623  mapdlsm  41646  mapdpglem1  41654  mapdindp0  41701  hlhilocv  41943  primrootscoprbij  42083  rntrclfvOAI  42678  ismrcd1  42685  ismrcd2  42686  coeq0i  42740  hbtlem6  43117  iocinico  43200  omabs2  43321  naddwordnexlem4  43390  trclubNEW  43608  ntrk2imkb  44026  isotone1  44037  k0004ss3  44142  iccdifprioo  45468  limsupequzmptlem  45683  cncfuni  45841  cncfiooicclem1  45848  dvresntr  45873  itgsubsticclem  45930  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  qndenserrn  46254  prsal  46273  intsaluni  46284  sssalgen  46290  dfsalgen2  46296  sge0split  46364  ismeannd  46422  caragensspw  46464  caragendifcl  46469  carageniuncl  46478  caratheodorylem1  46481  hoicvrrex  46511  ovnssle  46516  ovn02  46523  ovnsubadd  46527  hoidmv1le  46549  ovnlecvr2  46565  ovncvr2  46566  isvonmbl  46593  vonmblss  46595  ovolval4lem2  46605  ovnovollem1  46611  ovnovollem2  46612  incsmf  46697  decsmf  46722  uspgropssxp  47987  mreuniss  48695  restcls2lem  48708  restcls2  48709  cnneiima  48712