Theorem sseqtrd 3970

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  sseqtrrd  3971  sseqtrid  3976  3sstr3d  3988  uniintsn  4940  fssdmd  6704  oeeui  8565  nnaword2  8593  oaabs2  8612  naddword2  8656  erssxp  8695  fipwuni  9365  cantnflem3  9639  ficardun2  10151  ackbij1lem12  10179  ackbij1b  10187  fin1a2lem13  10362  winafp  10648  ioodisj  13479  reltrclfv  15023  prodss  15967  mrcssv  17636  mrcsscl  17642  mrcuni  17643  mressmrcd  17649  mreexexlem2d  17667  mreexexlem3d  17668  mreexfidimd  17672  subcss2  17866  resssetc  18115  funcsetcres2  18116  estrres  18161  poslubdg  18434  ipodrsfi  18561  acsmap2d  18577  mrelatlub  18584  mreclatBAD  18585  subsubmgm  18734  subsubm  18840  subsubg  19181  trivsubgd  19184  trivnsgd  19203  oppglsm  19672  subglsm  19703  lsmdisj  19711  gsumval3  19937  dprdres  20060  dprdss  20061  dprd2da  20074  dmdprdsplit2lem  20077  ablfac1b  20102  pgpfac1lem3  20109  subsubrng  20599  subsubrg  20634  rgspnval  20648  issubdrg  20816  islssd  20989  lspun  21041  lspssp  21042  lsslsp  21069  lsmssspx  21142  lspabs2  21177  lspabs3  21178  lspsolvlem  21199  lbsextlem3  21217  qsssubdrg  21465  obselocv  21767  lsslindf  21869  sraassa  21908  mplbas2  22082  gsumply1subr  22282  tgcl  23016  basgen  23035  tgfiss  23038  bastop1  23040  bastop2  23041  clsss2  23119  elcls3  23130  topssnei  23171  neiptopnei  23179  neitr  23227  restcls  23228  restlp  23230  ordtrest2  23251  iscncl  23316  cncls2  23320  cncls  23321  cnntr  23322  lmcls  23349  tgcmp  23448  cmpcld  23449  uncmp  23450  hauscmplem  23453  cmpfi  23455  clsconn  23477  2ndcsb  23496  2ndcctbss  23502  2ndcomap  23505  nllyrest  23533  1stckgenlem  23600  kgencn2  23604  kgen2cn  23606  ptbasfi  23628  txcld  23650  txcls  23651  txbasval  23653  neitx  23654  ptcld  23660  ptclsg  23662  txnlly  23684  hausdiag  23692  txkgen  23699  xkopt  23702  xkopjcn  23703  xkococnlem  23706  cnmpt1res  23723  cnmpt2res  23724  imasnopn  23737  imasncld  23738  imasncls  23739  qtopcld  23760  qtoprest  23764  qtopcmap  23766  kqcldsat  23780  kqreglem2  23789  kqnrmlem2  23791  hmeontr  23816  neifil  23927  fgtr  23937  trnei  23939  uffixfr  23970  uffix2  23971  uffixsn  23972  elflim  24018  flimclslem  24031  fclsopn  24061  fclscmpi  24076  fclscmp  24077  alexsubALTlem3  24096  alexsubALT  24098  ptcmplem3  24101  subgntr  24154  opnsubg  24155  clssubg  24156  clsnsg  24157  cldsubg  24158  tgpconncompeqg  24159  snclseqg  24163  tsmsgsum  24186  tsmsid  24187  tgptsmscld  24198  ustssco  24262  utop2nei  24297  utop3cls  24298  utopreg  24299  cnextucn  24349  ressprdsds  24418  lpbl  24550  met2ndci  24569  prdsxmslem2  24576  metustexhalf  24603  psmetutop  24614  tgioo  24843  metdstri  24899  metdseq0  24902  xlebnum  25014  clsocv  25299  metelcls  25354  metsscmetcld  25364  cmetss  25365  relcmpcmet  25367  cmpcmet  25368  minveclem4a  25479  uniioovol  25628  uniioombllem3  25634  limcres  25935  dvbss  25950  perfdvf  25952  dvreslem  25958  dvres2lem  25959  dvmptresicc  25965  dvcnp2  25969  dvaddbr  25987  dvmulbr  25988  dvcmulf  25994  dvcj  25999  dvnfre  26001  dvmptres2  26011  dvmptcmul  26013  dvmptntr  26020  dvlip2  26044  dvcnvrelem2  26067  ftc1cn  26092  dvntaylp  26421  taylthlem1  26423  ulmdvlem3  26452  pserulm  26472  nodense  27743  mulsproplem13  28208  mulsproplem14  28209  onsbnd  28361  shsub2  31484  spanssoc  31508  shub2  31542  ococin  31567  ssjo  31606  chub2  31667  spanpr  31739  elnlfn  32087  mdslj1i  32478  mdslmd3i  32491  mdexchi  32494  chirredlem1  32549  atcvat3i  32555  mdsymlem1  32562  mdsymlem5  32566  imadifxp  32760  fnpreimac  32832  suppovss  32843  symgcom2  33224  pmtrcnelor  33231  cycpmco2f1  33264  0ringsubrg  33392  erlval  33399  1fldgenq  33469  0ringidl  33567  elrspunidl  33574  0ringprmidl  33596  drngmxidl  33625  drngmxidlr  33626  idlsrgmulrss1  33667  idlsrgmulrss2  33668  1arithidomlem2  33692  ply1dg3rt0irred  33740  resssra  33844  lsssra  33845  drgextlsp  33851  lvecdim0  33864  lbslsat  33873  dimkerim  33884  fedgmullem2  33887  fedgmul  33888  fldgenfldext  33925  fldextrspunlsplem  33930  fldextrspunlsp  33931  fldextrspunlem1  33932  fldextrspunfld  33933  fldextrspundgdvdslem  33937  fldextrspundgdvds  33938  algextdeglem3  33976  algextdeglem4  33977  qtophaus  34093  locfinreflem  34097  rspecbas  34122  zarclssn  34130  zarmxt1  34137  zarcmplem  34138  fsumcvg4  34207  esum2d  34350  omsmon  34555  omssubadd  34557  carsgclctun  34578  sitgclg  34599  eulerpartlemgf  34636  reprpmtf1o  34880  cvmscld  35583  cvmliftmolem1  35591  cvmlift2lem9  35621  cvmlift2lem11  35623  cvmlift3lem6  35634  opnregcld  36650  ivthALT  36655  neibastop2  36681  fnemeet1  36686  fnejoin1  36688  pibt2  37871  poimirlem11  38090  poimirlem12  38091  poimirlem30  38109  ftc1cnnc  38151  sstotbnd  38234  ssbnd  38247  heibor1lem  38268  heiborlem3  38272  heibor  38280  lsmsat  39592  lssats  39596  lcvexchlem3  39620  lsatcvat3  39636  lkrscss  39682  lkrpssN  39747  pmod1i  40432  pclbtwnN  40481  pclunN  40482  pclss2polN  40505  pcl0N  40506  sspmaplubN  40509  paddunN  40511  pnonsingN  40517  pclfinclN  40534  osumcllem4N  40543  dia2dimlem13  41660  dvhopellsm  41701  dvadiaN  41712  dicelval1stN  41772  dicelval2nd  41773  dihssxp  41836  dihvalrel  41863  dochsscl  41952  dihoml4  41961  dochnoncon  41975  dvh3dim3N  42033  lcfrlem2  42127  lcfrlem5  42130  lcfr  42169  lcdlsp  42205  mapdsn  42225  mapdlsm  42248  mapdpglem1  42256  mapdindp0  42303  hlhilocv  42541  primrootscoprbij  42679  rntrclfvOAI  43232  ismrcd1  43239  ismrcd2  43240  coeq0i  43294  hbtlem6  43666  iocinico  43749  omabs2  43869  naddwordnexlem4  43938  trclubNEW  44155  ntrk2imkb  44573  isotone1  44584  k0004ss3  44689  iccdifprioo  46052  limsupequzmptlem  46262  cncfuni  46420  cncfiooicclem1  46427  dvresntr  46452  itgsubsticclem  46509  fourierdlem42  46683  fourierdlem48  46688  fourierdlem49  46689  fourierdlem50  46690  qndenserrn  46833  prsal  46852  intsaluni  46863  sssalgen  46869  dfsalgen2  46875  sge0split  46943  ismeannd  47001  caragensspw  47043  caragendifcl  47048  carageniuncl  47057  caratheodorylem1  47060  hoicvrrex  47090  ovnssle  47095  ovn02  47102  ovnsubadd  47106  hoidmv1le  47128  ovnlecvr2  47144  ovncvr2  47145  isvonmbl  47172  vonmblss  47174  ovolval4lem2  47184  ovnovollem1  47190  ovnovollem2  47191  incsmf  47276  decsmf  47301  uspgropssxp  48726  mreuniss  49481  restcls2lem  49494  restcls2  49495  cnneiima  49498  imassc  49734