Theorem sseqtrd 4049

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  sseqtrrd  4050  sseqtrid  4061  uniintsn  5009  fssdmd  6765  oeeui  8658  nnaword2  8686  oaabs2  8705  naddword2  8748  erssxp  8786  fipwuni  9495  cantnflem3  9760  ficardun2  10271  ackbij1lem12  10299  ackbij1b  10307  fin1a2lem13  10481  winafp  10766  ioodisj  13542  reltrclfv  15066  prodss  15995  mrcssv  17672  mrcsscl  17678  mrcuni  17679  mressmrcd  17685  mreexexlem2d  17703  mreexexlem3d  17704  mreexfidimd  17708  subcss2  17907  resssetc  18159  funcsetcres2  18160  estrres  18208  poslubdg  18484  ipodrsfi  18609  acsmap2d  18625  mrelatlub  18632  mreclatBAD  18633  subsubmgm  18748  subsubm  18851  subsubg  19189  trivsubgd  19193  trivnsgd  19212  oppglsm  19684  subglsm  19715  lsmdisj  19723  gsumval3  19949  dprdres  20072  dprdss  20073  dprd2da  20086  dmdprdsplit2lem  20089  ablfac1b  20114  pgpfac1lem3  20121  subsubrng  20589  subsubrg  20626  issubdrg  20803  islssd  20956  lspun  21008  lspssp  21009  lsslsp  21036  lsslspOLD  21037  lsmssspx  21110  lspabs2  21145  lspabs3  21146  lspsolvlem  21167  lbsextlem3  21185  qsssubdrg  21467  obselocv  21771  lsslindf  21873  sraassa  21912  mplbas2  22083  gsumply1subr  22256  tgcl  22997  basgen  23016  tgfiss  23019  bastop1  23021  bastop2  23022  clsss2  23101  elcls3  23112  topssnei  23153  neiptopnei  23161  neitr  23209  restcls  23210  restlp  23212  ordtrest2  23233  iscncl  23298  cncls2  23302  cncls  23303  cnntr  23304  lmcls  23331  tgcmp  23430  cmpcld  23431  uncmp  23432  hauscmplem  23435  cmpfi  23437  clsconn  23459  2ndcsb  23478  2ndcctbss  23484  2ndcomap  23487  nllyrest  23515  1stckgenlem  23582  kgencn2  23586  kgen2cn  23588  ptbasfi  23610  txcld  23632  txcls  23633  txbasval  23635  neitx  23636  ptcld  23642  ptclsg  23644  txnlly  23666  hausdiag  23674  txkgen  23681  xkopt  23684  xkopjcn  23685  xkococnlem  23688  cnmpt1res  23705  cnmpt2res  23706  imasnopn  23719  imasncld  23720  imasncls  23721  qtopcld  23742  qtoprest  23746  qtopcmap  23748  kqcldsat  23762  kqreglem2  23771  kqnrmlem2  23773  hmeontr  23798  neifil  23909  fgtr  23919  trnei  23921  uffixfr  23952  uffix2  23953  uffixsn  23954  elflim  24000  flimclslem  24013  fclsopn  24043  fclscmpi  24058  fclscmp  24059  alexsubALTlem3  24078  alexsubALT  24080  ptcmplem3  24083  subgntr  24136  opnsubg  24137  clssubg  24138  clsnsg  24139  cldsubg  24140  tgpconncompeqg  24141  snclseqg  24145  tsmsgsum  24168  tsmsid  24169  tgptsmscld  24180  ustssco  24244  utop2nei  24280  utop3cls  24281  utopreg  24282  cnextucn  24333  ressprdsds  24402  lpbl  24537  met2ndci  24556  prdsxmslem2  24563  metustexhalf  24590  psmetutop  24601  tgioo  24837  metdstri  24892  metdseq0  24895  xlebnum  25016  clsocv  25303  metelcls  25358  metsscmetcld  25368  cmetss  25369  relcmpcmet  25371  cmpcmet  25372  minveclem4a  25483  uniioovol  25633  uniioombllem3  25639  limcres  25941  dvbss  25956  perfdvf  25958  dvreslem  25964  dvres2lem  25965  dvmptresicc  25971  dvcnp2  25975  dvcnp2OLD  25976  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcmulf  26002  dvcj  26008  dvnfre  26010  dvmptres2  26020  dvmptcmul  26022  dvmptntr  26029  dvlip2  26054  dvcnvrelem2  26077  ftc1cn  26104  dvntaylp  26431  taylthlem1  26433  ulmdvlem3  26463  pserulm  26483  nodense  27755  mulsproplem13  28172  mulsproplem14  28173  shsub2  31357  spanssoc  31381  shub2  31415  ococin  31440  ssjo  31479  chub2  31540  spanpr  31612  elnlfn  31960  mdslj1i  32351  mdslmd3i  32364  mdexchi  32367  chirredlem1  32422  atcvat3i  32428  mdsymlem1  32435  mdsymlem5  32439  imadifxp  32623  fnpreimac  32689  suppovss  32697  symgcom2  33077  pmtrcnelor  33084  cycpmco2f1  33117  0ringsubrg  33223  erlval  33230  1fldgenq  33289  0ringidl  33414  elrspunidl  33421  0ringprmidl  33442  drngmxidl  33470  drngmxidlr  33471  idlsrgmulrss1  33504  idlsrgmulrss2  33505  1arithidomlem2  33529  ply1dg3rt0irred  33572  resssra  33602  lsssra  33603  drgextlsp  33608  lvecdim0  33619  lbslsat  33629  dimkerim  33640  fedgmullem2  33643  fedgmul  33644  fldgenfldext  33678  algextdeglem3  33710  algextdeglem4  33711  qtophaus  33782  locfinreflem  33786  rspecbas  33811  zarclssn  33819  zarmxt1  33826  zarcmplem  33827  fsumcvg4  33896  esum2d  34057  omsmon  34263  omssubadd  34265  carsgclctun  34286  sitgclg  34307  eulerpartlemgf  34344  reprpmtf1o  34603  cvmscld  35241  cvmliftmolem1  35249  cvmlift2lem9  35279  cvmlift2lem11  35281  cvmlift3lem6  35292  opnregcld  36296  ivthALT  36301  neibastop2  36327  fnemeet1  36332  fnejoin1  36334  pibt2  37383  poimirlem11  37591  poimirlem12  37592  poimirlem30  37610  ftc1cnnc  37652  sstotbnd  37735  ssbnd  37748  heibor1lem  37769  heiborlem3  37773  heibor  37781  lsmsat  38964  lssats  38968  lcvexchlem3  38992  lsatcvat3  39008  lkrscss  39054  lkrpssN  39119  pmod1i  39805  pclbtwnN  39854  pclunN  39855  pclss2polN  39878  pcl0N  39879  sspmaplubN  39882  paddunN  39884  pnonsingN  39890  pclfinclN  39907  osumcllem4N  39916  dia2dimlem13  41033  dvhopellsm  41074  dvadiaN  41085  dicelval1stN  41145  dicelval2nd  41146  dihssxp  41209  dihvalrel  41236  dochsscl  41325  dihoml4  41334  dochnoncon  41348  dvh3dim3N  41406  lcfrlem2  41500  lcfrlem5  41503  lcfr  41542  lcdlsp  41578  mapdsn  41598  mapdlsm  41621  mapdpglem1  41629  mapdindp0  41676  hlhilocv  41918  primrootscoprbij  42059  rntrclfvOAI  42647  ismrcd1  42654  ismrcd2  42655  coeq0i  42709  hbtlem6  43086  rgspnval  43125  iocinico  43173  omabs2  43294  naddwordnexlem4  43363  trclubNEW  43581  ntrk2imkb  43999  isotone1  44010  k0004ss3  44115  iccdifprioo  45434  limsupequzmptlem  45649  cncfuni  45807  cncfiooicclem1  45814  dvresntr  45839  itgsubsticclem  45896  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  qndenserrn  46220  prsal  46239  intsaluni  46250  sssalgen  46256  dfsalgen2  46262  sge0split  46330  ismeannd  46388  caragensspw  46430  caragendifcl  46435  carageniuncl  46444  caratheodorylem1  46447  hoicvrrex  46477  ovnssle  46482  ovn02  46489  ovnsubadd  46493  hoidmv1le  46515  ovnlecvr2  46531  ovncvr2  46532  isvonmbl  46559  vonmblss  46561  ovolval4lem2  46571  ovnovollem1  46577  ovnovollem2  46578  incsmf  46663  decsmf  46688  uspgropssxp  47867  mreuniss  48579  restcls2lem  48592  restcls2  48593  cnneiima  48596