Theorem sseqtrd 3983

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  sseqtrrd  3984  sseqtrid  3989  3sstr3d  4001  uniintsn  4949  fssdmd  6706  oeeui  8566  nnaword2  8594  oaabs2  8613  naddword2  8656  erssxp  8694  fipwuni  9377  cantnflem3  9644  ficardun2  10155  ackbij1lem12  10183  ackbij1b  10191  fin1a2lem13  10365  winafp  10650  ioodisj  13443  reltrclfv  14983  prodss  15913  mrcssv  17575  mrcsscl  17581  mrcuni  17582  mressmrcd  17588  mreexexlem2d  17606  mreexexlem3d  17607  mreexfidimd  17611  subcss2  17805  resssetc  18054  funcsetcres2  18055  estrres  18100  poslubdg  18373  ipodrsfi  18498  acsmap2d  18514  mrelatlub  18521  mreclatBAD  18522  subsubmgm  18637  subsubm  18743  subsubg  19081  trivsubgd  19085  trivnsgd  19104  oppglsm  19572  subglsm  19603  lsmdisj  19611  gsumval3  19837  dprdres  19960  dprdss  19961  dprd2da  19974  dmdprdsplit2lem  19977  ablfac1b  20002  pgpfac1lem3  20009  subsubrng  20472  subsubrg  20507  rgspnval  20521  issubdrg  20689  islssd  20841  lspun  20893  lspssp  20894  lsslsp  20921  lsslspOLD  20922  lsmssspx  20995  lspabs2  21030  lspabs3  21031  lspsolvlem  21052  lbsextlem3  21070  qsssubdrg  21343  obselocv  21637  lsslindf  21739  sraassa  21778  mplbas2  21949  gsumply1subr  22118  tgcl  22856  basgen  22875  tgfiss  22878  bastop1  22880  bastop2  22881  clsss2  22959  elcls3  22970  topssnei  23011  neiptopnei  23019  neitr  23067  restcls  23068  restlp  23070  ordtrest2  23091  iscncl  23156  cncls2  23160  cncls  23161  cnntr  23162  lmcls  23189  tgcmp  23288  cmpcld  23289  uncmp  23290  hauscmplem  23293  cmpfi  23295  clsconn  23317  2ndcsb  23336  2ndcctbss  23342  2ndcomap  23345  nllyrest  23373  1stckgenlem  23440  kgencn2  23444  kgen2cn  23446  ptbasfi  23468  txcld  23490  txcls  23491  txbasval  23493  neitx  23494  ptcld  23500  ptclsg  23502  txnlly  23524  hausdiag  23532  txkgen  23539  xkopt  23542  xkopjcn  23543  xkococnlem  23546  cnmpt1res  23563  cnmpt2res  23564  imasnopn  23577  imasncld  23578  imasncls  23579  qtopcld  23600  qtoprest  23604  qtopcmap  23606  kqcldsat  23620  kqreglem2  23629  kqnrmlem2  23631  hmeontr  23656  neifil  23767  fgtr  23777  trnei  23779  uffixfr  23810  uffix2  23811  uffixsn  23812  elflim  23858  flimclslem  23871  fclsopn  23901  fclscmpi  23916  fclscmp  23917  alexsubALTlem3  23936  alexsubALT  23938  ptcmplem3  23941  subgntr  23994  opnsubg  23995  clssubg  23996  clsnsg  23997  cldsubg  23998  tgpconncompeqg  23999  snclseqg  24003  tsmsgsum  24026  tsmsid  24027  tgptsmscld  24038  ustssco  24102  utop2nei  24138  utop3cls  24139  utopreg  24140  cnextucn  24190  ressprdsds  24259  lpbl  24391  met2ndci  24410  prdsxmslem2  24417  metustexhalf  24444  psmetutop  24455  tgioo  24684  metdstri  24740  metdseq0  24743  xlebnum  24864  clsocv  25150  metelcls  25205  metsscmetcld  25215  cmetss  25216  relcmpcmet  25218  cmpcmet  25219  minveclem4a  25330  uniioovol  25480  uniioombllem3  25486  limcres  25787  dvbss  25802  perfdvf  25804  dvreslem  25810  dvres2lem  25811  dvmptresicc  25817  dvcnp2  25821  dvcnp2OLD  25822  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcmulf  25848  dvcj  25854  dvnfre  25856  dvmptres2  25866  dvmptcmul  25868  dvmptntr  25875  dvlip2  25900  dvcnvrelem2  25923  ftc1cn  25950  dvntaylp  26279  taylthlem1  26281  ulmdvlem3  26311  pserulm  26331  nodense  27604  mulsproplem13  28031  mulsproplem14  28032  shsub2  31254  spanssoc  31278  shub2  31312  ococin  31337  ssjo  31376  chub2  31437  spanpr  31509  elnlfn  31857  mdslj1i  32248  mdslmd3i  32261  mdexchi  32264  chirredlem1  32319  atcvat3i  32325  mdsymlem1  32332  mdsymlem5  32336  imadifxp  32530  fnpreimac  32595  suppovss  32604  symgcom2  33041  pmtrcnelor  33048  cycpmco2f1  33081  0ringsubrg  33202  erlval  33209  1fldgenq  33272  0ringidl  33392  elrspunidl  33399  0ringprmidl  33420  drngmxidl  33448  drngmxidlr  33449  idlsrgmulrss1  33482  idlsrgmulrss2  33483  1arithidomlem2  33507  ply1dg3rt0irred  33551  resssra  33583  lsssra  33584  drgextlsp  33589  lvecdim0  33602  lbslsat  33612  dimkerim  33623  fedgmullem2  33626  fedgmul  33627  fldgenfldext  33663  fldextrspunlsplem  33668  fldextrspunlsp  33669  fldextrspunlem1  33670  fldextrspunfld  33671  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  algextdeglem3  33709  algextdeglem4  33710  qtophaus  33826  locfinreflem  33830  rspecbas  33855  zarclssn  33863  zarmxt1  33870  zarcmplem  33871  fsumcvg4  33940  esum2d  34083  omsmon  34289  omssubadd  34291  carsgclctun  34312  sitgclg  34333  eulerpartlemgf  34370  reprpmtf1o  34617  cvmscld  35260  cvmliftmolem1  35268  cvmlift2lem9  35298  cvmlift2lem11  35300  cvmlift3lem6  35311  opnregcld  36318  ivthALT  36323  neibastop2  36349  fnemeet1  36354  fnejoin1  36356  pibt2  37405  poimirlem11  37625  poimirlem12  37626  poimirlem30  37644  ftc1cnnc  37686  sstotbnd  37769  ssbnd  37782  heibor1lem  37803  heiborlem3  37807  heibor  37815  lsmsat  39001  lssats  39005  lcvexchlem3  39029  lsatcvat3  39045  lkrscss  39091  lkrpssN  39156  pmod1i  39842  pclbtwnN  39891  pclunN  39892  pclss2polN  39915  pcl0N  39916  sspmaplubN  39919  paddunN  39921  pnonsingN  39927  pclfinclN  39944  osumcllem4N  39953  dia2dimlem13  41070  dvhopellsm  41111  dvadiaN  41122  dicelval1stN  41182  dicelval2nd  41183  dihssxp  41246  dihvalrel  41273  dochsscl  41362  dihoml4  41371  dochnoncon  41385  dvh3dim3N  41443  lcfrlem2  41537  lcfrlem5  41540  lcfr  41579  lcdlsp  41615  mapdsn  41635  mapdlsm  41658  mapdpglem1  41666  mapdindp0  41713  hlhilocv  41951  primrootscoprbij  42090  rntrclfvOAI  42679  ismrcd1  42686  ismrcd2  42687  coeq0i  42741  hbtlem6  43118  iocinico  43201  omabs2  43321  naddwordnexlem4  43390  trclubNEW  43608  ntrk2imkb  44026  isotone1  44037  k0004ss3  44142  iccdifprioo  45514  limsupequzmptlem  45726  cncfuni  45884  cncfiooicclem1  45891  dvresntr  45916  itgsubsticclem  45973  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  qndenserrn  46297  prsal  46316  intsaluni  46327  sssalgen  46333  dfsalgen2  46339  sge0split  46407  ismeannd  46465  caragensspw  46507  caragendifcl  46512  carageniuncl  46521  caratheodorylem1  46524  hoicvrrex  46554  ovnssle  46559  ovn02  46566  ovnsubadd  46570  hoidmv1le  46592  ovnlecvr2  46608  ovncvr2  46609  isvonmbl  46636  vonmblss  46638  ovolval4lem2  46648  ovnovollem1  46654  ovnovollem2  46655  incsmf  46740  decsmf  46765  uspgropssxp  48132  mreuniss  48888  restcls2lem  48901  restcls2  48902  cnneiima  48905  imassc  49142