Theorem sseqtrd 3971

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919

This theorem is referenced by:  sseqtrrd  3972  sseqtrid  3977  3sstr3d  3989  uniintsn  4935  fssdmd  6669  oeeui  8517  nnaword2  8545  oaabs2  8564  naddword2  8607  erssxp  8645  fipwuni  9310  cantnflem3  9581  ficardun2  10093  ackbij1lem12  10121  ackbij1b  10129  fin1a2lem13  10303  winafp  10588  ioodisj  13382  reltrclfv  14924  prodss  15854  mrcssv  17520  mrcsscl  17526  mrcuni  17527  mressmrcd  17533  mreexexlem2d  17551  mreexexlem3d  17552  mreexfidimd  17556  subcss2  17750  resssetc  17999  funcsetcres2  18000  estrres  18045  poslubdg  18318  ipodrsfi  18445  acsmap2d  18461  mrelatlub  18468  mreclatBAD  18469  subsubmgm  18618  subsubm  18724  subsubg  19062  trivsubgd  19066  trivnsgd  19085  oppglsm  19555  subglsm  19586  lsmdisj  19594  gsumval3  19820  dprdres  19943  dprdss  19944  dprd2da  19957  dmdprdsplit2lem  19960  ablfac1b  19985  pgpfac1lem3  19992  subsubrng  20479  subsubrg  20514  rgspnval  20528  issubdrg  20696  islssd  20869  lspun  20921  lspssp  20922  lsslsp  20949  lsslspOLD  20950  lsmssspx  21023  lspabs2  21058  lspabs3  21059  lspsolvlem  21080  lbsextlem3  21098  qsssubdrg  21364  obselocv  21666  lsslindf  21768  sraassa  21807  mplbas2  21978  gsumply1subr  22147  tgcl  22885  basgen  22904  tgfiss  22907  bastop1  22909  bastop2  22910  clsss2  22988  elcls3  22999  topssnei  23040  neiptopnei  23048  neitr  23096  restcls  23097  restlp  23099  ordtrest2  23120  iscncl  23185  cncls2  23189  cncls  23190  cnntr  23191  lmcls  23218  tgcmp  23317  cmpcld  23318  uncmp  23319  hauscmplem  23322  cmpfi  23324  clsconn  23346  2ndcsb  23365  2ndcctbss  23371  2ndcomap  23374  nllyrest  23402  1stckgenlem  23469  kgencn2  23473  kgen2cn  23475  ptbasfi  23497  txcld  23519  txcls  23520  txbasval  23522  neitx  23523  ptcld  23529  ptclsg  23531  txnlly  23553  hausdiag  23561  txkgen  23568  xkopt  23571  xkopjcn  23572  xkococnlem  23575  cnmpt1res  23592  cnmpt2res  23593  imasnopn  23606  imasncld  23607  imasncls  23608  qtopcld  23629  qtoprest  23633  qtopcmap  23635  kqcldsat  23649  kqreglem2  23658  kqnrmlem2  23660  hmeontr  23685  neifil  23796  fgtr  23806  trnei  23808  uffixfr  23839  uffix2  23840  uffixsn  23841  elflim  23887  flimclslem  23900  fclsopn  23930  fclscmpi  23945  fclscmp  23946  alexsubALTlem3  23965  alexsubALT  23967  ptcmplem3  23970  subgntr  24023  opnsubg  24024  clssubg  24025  clsnsg  24026  cldsubg  24027  tgpconncompeqg  24028  snclseqg  24032  tsmsgsum  24055  tsmsid  24056  tgptsmscld  24067  ustssco  24131  utop2nei  24166  utop3cls  24167  utopreg  24168  cnextucn  24218  ressprdsds  24287  lpbl  24419  met2ndci  24438  prdsxmslem2  24445  metustexhalf  24472  psmetutop  24483  tgioo  24712  metdstri  24768  metdseq0  24771  xlebnum  24892  clsocv  25178  metelcls  25233  metsscmetcld  25243  cmetss  25244  relcmpcmet  25246  cmpcmet  25247  minveclem4a  25358  uniioovol  25508  uniioombllem3  25514  limcres  25815  dvbss  25830  perfdvf  25832  dvreslem  25838  dvres2lem  25839  dvmptresicc  25845  dvcnp2  25849  dvcnp2OLD  25850  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvcmulf  25876  dvcj  25882  dvnfre  25884  dvmptres2  25894  dvmptcmul  25896  dvmptntr  25903  dvlip2  25928  dvcnvrelem2  25951  ftc1cn  25978  dvntaylp  26307  taylthlem1  26309  ulmdvlem3  26339  pserulm  26359  nodense  27632  mulsproplem13  28068  mulsproplem14  28069  shsub2  31303  spanssoc  31327  shub2  31361  ococin  31386  ssjo  31425  chub2  31486  spanpr  31558  elnlfn  31906  mdslj1i  32297  mdslmd3i  32310  mdexchi  32313  chirredlem1  32368  atcvat3i  32374  mdsymlem1  32381  mdsymlem5  32385  imadifxp  32579  fnpreimac  32651  suppovss  32660  symgcom2  33051  pmtrcnelor  33058  cycpmco2f1  33091  0ringsubrg  33216  erlval  33223  1fldgenq  33286  0ringidl  33384  elrspunidl  33391  0ringprmidl  33412  drngmxidl  33440  drngmxidlr  33441  idlsrgmulrss1  33474  idlsrgmulrss2  33475  1arithidomlem2  33499  ply1dg3rt0irred  33544  resssra  33597  lsssra  33598  drgextlsp  33604  lvecdim0  33617  lbslsat  33627  dimkerim  33638  fedgmullem2  33641  fedgmul  33642  fldgenfldext  33679  fldextrspunlsplem  33684  fldextrspunlsp  33685  fldextrspunlem1  33686  fldextrspunfld  33687  fldextrspundgdvdslem  33691  fldextrspundgdvds  33692  algextdeglem3  33730  algextdeglem4  33731  qtophaus  33847  locfinreflem  33851  rspecbas  33876  zarclssn  33884  zarmxt1  33891  zarcmplem  33892  fsumcvg4  33961  esum2d  34104  omsmon  34309  omssubadd  34311  carsgclctun  34332  sitgclg  34353  eulerpartlemgf  34390  reprpmtf1o  34637  cvmscld  35315  cvmliftmolem1  35323  cvmlift2lem9  35353  cvmlift2lem11  35355  cvmlift3lem6  35366  opnregcld  36370  ivthALT  36375  neibastop2  36401  fnemeet1  36406  fnejoin1  36408  pibt2  37457  poimirlem11  37677  poimirlem12  37678  poimirlem30  37696  ftc1cnnc  37738  sstotbnd  37821  ssbnd  37834  heibor1lem  37855  heiborlem3  37859  heibor  37867  lsmsat  39053  lssats  39057  lcvexchlem3  39081  lsatcvat3  39097  lkrscss  39143  lkrpssN  39208  pmod1i  39893  pclbtwnN  39942  pclunN  39943  pclss2polN  39966  pcl0N  39967  sspmaplubN  39970  paddunN  39972  pnonsingN  39978  pclfinclN  39995  osumcllem4N  40004  dia2dimlem13  41121  dvhopellsm  41162  dvadiaN  41173  dicelval1stN  41233  dicelval2nd  41234  dihssxp  41297  dihvalrel  41324  dochsscl  41413  dihoml4  41422  dochnoncon  41436  dvh3dim3N  41494  lcfrlem2  41588  lcfrlem5  41591  lcfr  41630  lcdlsp  41666  mapdsn  41686  mapdlsm  41709  mapdpglem1  41717  mapdindp0  41764  hlhilocv  42002  primrootscoprbij  42141  rntrclfvOAI  42730  ismrcd1  42737  ismrcd2  42738  coeq0i  42792  hbtlem6  43168  iocinico  43251  omabs2  43371  naddwordnexlem4  43440  trclubNEW  43658  ntrk2imkb  44076  isotone1  44087  k0004ss3  44192  iccdifprioo  45562  limsupequzmptlem  45772  cncfuni  45930  cncfiooicclem1  45937  dvresntr  45962  itgsubsticclem  46019  fourierdlem42  46193  fourierdlem48  46198  fourierdlem49  46199  fourierdlem50  46200  qndenserrn  46343  prsal  46362  intsaluni  46373  sssalgen  46379  dfsalgen2  46385  sge0split  46453  ismeannd  46511  caragensspw  46553  caragendifcl  46558  carageniuncl  46567  caratheodorylem1  46570  hoicvrrex  46600  ovnssle  46605  ovn02  46612  ovnsubadd  46616  hoidmv1le  46638  ovnlecvr2  46654  ovncvr2  46655  isvonmbl  46682  vonmblss  46684  ovolval4lem2  46694  ovnovollem1  46700  ovnovollem2  46701  incsmf  46786  decsmf  46811  uspgropssxp  48181  mreuniss  48937  restcls2lem  48950  restcls2  48951  cnneiima  48954  imassc  49191