Theorem sseqtrd 3962

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  sseqtrrd  3963  uniintsn  4919  fssdmd  6628  oeeui  8442  nnaword2  8470  oaabs2  8488  erssxp  8530  fipwuni  9194  cantnflem3  9458  ficardun2  9967  ficardun2OLD  9968  ackbij1lem12  9996  ackbij1b  10004  fin1a2lem13  10177  winafp  10462  ioodisj  13223  reltrclfv  14737  prodss  15666  mrcssv  17332  mrcsscl  17338  mrcuni  17339  mressmrcd  17345  mreexexlem2d  17363  mreexexlem3d  17364  mreexfidimd  17368  subcss2  17567  resssetc  17816  funcsetcres2  17817  estrres  17865  poslubdg  18141  ipodrsfi  18266  acsmap2d  18282  mrelatlub  18289  mreclatBAD  18290  subsubm  18464  subsubg  18787  trivsubgd  18790  trivnsgd  18809  oppglsm  19256  subglsm  19288  lsmdisj  19296  gsumval3  19517  dprdres  19640  dprdss  19641  dprd2da  19654  dmdprdsplit2lem  19657  ablfac1b  19682  pgpfac1lem3  19689  issubdrg  20058  subsubrg  20059  islssd  20206  lspun  20258  lspssp  20259  lsslsp  20286  lsmssspx  20359  lspabs2  20391  lspabs3  20392  lspsolvlem  20413  lbsextlem3  20431  qsssubdrg  20666  obselocv  20944  lsslindf  21046  mplbas2  21252  gsumply1subr  21414  tgcl  22128  basgen  22147  tgfiss  22150  bastop1  22152  bastop2  22153  clsss2  22232  elcls3  22243  topssnei  22284  neiptopnei  22292  neitr  22340  restcls  22341  restlp  22343  ordtrest2  22364  iscncl  22429  cncls2  22433  cncls  22434  cnntr  22435  lmcls  22462  tgcmp  22561  cmpcld  22562  uncmp  22563  hauscmplem  22566  cmpfi  22568  clsconn  22590  2ndcsb  22609  2ndcctbss  22615  2ndcomap  22618  nllyrest  22646  1stckgenlem  22713  kgencn2  22717  kgen2cn  22719  ptbasfi  22741  txcld  22763  txcls  22764  txbasval  22766  neitx  22767  ptcld  22773  ptclsg  22775  txnlly  22797  hausdiag  22805  txkgen  22812  xkopt  22815  xkopjcn  22816  xkococnlem  22819  cnmpt1res  22836  cnmpt2res  22837  imasnopn  22850  imasncld  22851  imasncls  22852  qtopcld  22873  qtoprest  22877  qtopcmap  22879  kqcldsat  22893  kqreglem2  22902  kqnrmlem2  22904  hmeontr  22929  neifil  23040  fgtr  23050  trnei  23052  uffixfr  23083  uffix2  23084  uffixsn  23085  elflim  23131  flimclslem  23144  fclsopn  23174  fclscmpi  23189  fclscmp  23190  alexsubALTlem3  23209  alexsubALT  23211  ptcmplem3  23214  subgntr  23267  opnsubg  23268  clssubg  23269  clsnsg  23270  cldsubg  23271  tgpconncompeqg  23272  snclseqg  23276  tsmsgsum  23299  tsmsid  23300  tgptsmscld  23311  ustssco  23375  utop2nei  23411  utop3cls  23412  utopreg  23413  cnextucn  23464  ressprdsds  23533  lpbl  23668  met2ndci  23687  prdsxmslem2  23694  metustexhalf  23721  psmetutop  23732  tgioo  23968  metdstri  24023  metdseq0  24026  xlebnum  24137  clsocv  24423  metelcls  24478  metsscmetcld  24488  cmetss  24489  relcmpcmet  24491  cmpcmet  24492  minveclem4a  24603  uniioovol  24752  uniioombllem3  24758  limcres  25059  dvbss  25074  perfdvf  25076  dvreslem  25082  dvres2lem  25083  dvmptresicc  25089  dvcnp2  25093  dvaddbr  25111  dvmulbr  25112  dvcmulf  25118  dvcj  25123  dvnfre  25125  dvmptres2  25135  dvmptcmul  25137  dvmptntr  25144  dvlip2  25168  dvcnvrelem2  25191  ftc1cn  25216  dvntaylp  25539  taylthlem1  25541  ulmdvlem3  25570  pserulm  25590  shsub2  29696  spanssoc  29720  shub2  29754  ococin  29779  ssjo  29818  chub2  29879  spanpr  29951  elnlfn  30299  mdslj1i  30690  mdslmd3i  30703  mdexchi  30706  chirredlem1  30761  atcvat3i  30767  mdsymlem1  30774  mdsymlem5  30778  imadifxp  30949  fnpreimac  31017  suppovss  31026  symgcom2  31362  pmtrcnelor  31369  cycpmco2f1  31400  0ringidl  31614  elrspunidl  31615  0ringprmidl  31634  idlsrgmulrss1  31665  idlsrgmulrss2  31666  drgextlsp  31690  lvecdim0  31699  lbslsat  31708  dimkerim  31717  fedgmullem2  31720  fedgmul  31721  qtophaus  31795  locfinreflem  31799  rspecbas  31824  zarclssn  31832  zarmxt1  31839  zarcmplem  31840  fsumcvg4  31909  esum2d  32070  omsmon  32274  omssubadd  32276  carsgclctun  32297  sitgclg  32318  eulerpartlemgf  32355  reprpmtf1o  32615  cvmscld  33244  cvmliftmolem1  33252  cvmlift2lem9  33282  cvmlift2lem11  33284  cvmlift3lem6  33295  nodense  33904  opnregcld  34528  ivthALT  34533  neibastop2  34559  fnemeet1  34564  fnejoin1  34566  pibt2  35597  poimirlem11  35797  poimirlem12  35798  poimirlem30  35816  ftc1cnnc  35858  sstotbnd  35942  ssbnd  35955  heibor1lem  35976  heiborlem3  35980  heibor  35988  lsmsat  37029  lssats  37033  lcvexchlem3  37057  lsatcvat3  37073  lkrscss  37119  lkrpssN  37184  pmod1i  37869  pclbtwnN  37918  pclunN  37919  pclss2polN  37942  pcl0N  37943  sspmaplubN  37946  paddunN  37948  pnonsingN  37954  pclfinclN  37971  osumcllem4N  37980  dia2dimlem13  39097  dvhopellsm  39138  dvadiaN  39149  dicelval1stN  39209  dicelval2nd  39210  dihssxp  39273  dihvalrel  39300  dochsscl  39389  dihoml4  39398  dochnoncon  39412  dvh3dim3N  39470  lcfrlem2  39564  lcfrlem5  39567  lcfr  39606  lcdlsp  39642  mapdsn  39662  mapdlsm  39685  mapdpglem1  39693  mapdindp0  39740  hlhilocv  39982  rntrclfvOAI  40520  ismrcd1  40527  ismrcd2  40528  coeq0i  40582  hbtlem6  40961  rgspnval  41000  iocinico  41050  trclubNEW  41234  ntrk2imkb  41654  isotone1  41665  k0004ss3  41770  iccdifprioo  43061  limsupequzmptlem  43276  cncfuni  43434  cncfiooicclem1  43441  dvresntr  43466  itgsubsticclem  43523  fourierdlem42  43697  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  qndenserrn  43847  prsal  43866  intsaluni  43875  sssalgen  43881  dfsalgen2  43887  sge0split  43954  ismeannd  44012  caragensspw  44054  caragendifcl  44059  carageniuncl  44068  caratheodorylem1  44071  hoicvrrex  44101  ovnssle  44106  ovn02  44113  ovnsubadd  44117  hoidmv1le  44139  ovnlecvr2  44155  ovncvr2  44156  isvonmbl  44183  vonmblss  44185  ovolval4lem2  44195  ovnovollem1  44201  ovnovollem2  44202  incsmf  44287  decsmf  44312  uspgropssxp  45317  subsubmgm  45362  mreuniss  46204  restcls2lem  46217  restcls2  46218  cnneiima  46221