Theorem sseqtrd 3967

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  sseqtrrd  3968  sseqtrid  3973  3sstr3d  3985  uniintsn  4945  fssdmd  6726  oeeui  8604  nnaword2  8632  oaabs2  8651  naddword2  8695  erssxp  8734  fipwuni  9411  cantnflem3  9685  ficardun2  10273  ackbij1lem12  10301  ackbij1b  10309  fin1a2lem13  10483  winafp  10775  ioodisj  13606  reltrclfv  15163  prodss  16107  mrcssv  17781  mrcsscl  17787  mrcuni  17788  mressmrcd  17794  mreexexlem2d  17812  mreexexlem3d  17813  mreexfidimd  17817  subcss2  18011  resssetc  18260  funcsetcres2  18261  estrres  18306  poslubdg  18579  ipodrsfi  18706  acsmap2d  18722  mrelatlub  18729  mreclatBAD  18730  subsubmgm  18892  subsubm  19005  subsubg  19353  trivsubgd  19356  trivnsgd  19375  oppglsm  19849  subglsm  19880  lsmdisj  19888  gsumval3  20114  dprdres  20237  dprdss  20238  dprd2da  20251  dmdprdsplit2lem  20254  ablfac1b  20279  pgpfac1lem3  20286  subsubrng  20808  subsubrg  20843  rgspnval  20857  issubdrg  21030  islssd  21203  lspun  21255  lspssp  21256  lsslsp  21283  lsmssspx  21356  lspabs2  21391  lspabs3  21392  lspsolvlem  21413  lbsextlem3  21431  0ringidl  21507  0ringprmidl  21626  qsssubdrg  21725  obselocv  22027  lsslindf  22129  sraassa  22170  mplbas2  22344  gsumply1subr  22544  tgcl  23280  basgen  23299  tgfiss  23302  bastop1  23304  bastop2  23305  clsss2  23383  elcls3  23394  topssnei  23435  neiptopnei  23443  neitr  23491  restcls  23492  restlp  23494  ordtrest2  23515  iscncl  23580  cncls2  23584  cncls  23585  cnntr  23586  lmcls  23613  tgcmp  23712  cmpcld  23713  uncmp  23714  hauscmplem  23717  cmpfi  23719  clsconn  23741  2ndcsb  23760  2ndcctbss  23767  2ndcomap  23770  nllyrest  23798  1stckgenlem  23865  kgencn2  23869  kgen2cn  23871  ptbasfi  23893  txcld  23915  txcls  23916  txbasval  23918  neitx  23919  ptcld  23925  ptclsg  23927  txnlly  23949  hausdiag  23957  txkgen  23964  xkopt  23967  xkopjcn  23968  xkococnlem  23971  cnmpt1res  23988  cnmpt2res  23989  imasnopn  24002  imasncld  24003  imasncls  24004  qtopcld  24025  qtoprest  24029  qtopcmap  24031  kqcldsat  24045  kqreglem2  24054  kqnrmlem2  24056  hmeontr  24081  neifil  24192  fgtr  24202  trnei  24204  uffixfr  24235  uffix2  24236  uffixsn  24237  elflim  24283  flimclslem  24296  fclsopn  24326  fclscmpi  24341  fclscmp  24342  alexsubALTlem3  24361  alexsubALT  24363  ptcmplem3  24366  subgntr  24419  opnsubg  24420  clssubg  24421  clsnsg  24422  cldsubg  24423  tgpconncompeqg  24424  snclseqg  24428  tsmsgsum  24451  tsmsid  24452  tgptsmscld  24463  ustssco  24527  utop2nei  24562  utop3cls  24563  utopreg  24564  cnextucn  24614  ressprdsds  24683  lpbl  24815  met2ndci  24834  prdsxmslem2  24841  metustexhalf  24868  psmetutop  24879  tgioo  25108  metdstri  25164  metdseq0  25167  xlebnum  25279  clsocv  25564  metelcls  25619  metsscmetcld  25629  cmetss  25630  relcmpcmet  25632  cmpcmet  25633  minveclem4a  25744  uniioovol  25893  uniioombllem3  25899  limcres  26199  dvbss  26214  perfdvf  26216  dvreslem  26222  dvres2lem  26223  dvmptresicc  26229  dvcnp2  26233  dvaddbr  26251  dvmulbr  26252  dvcmulf  26258  dvcj  26263  dvnfre  26265  dvmptres2  26275  dvmptcmul  26277  dvmptntr  26284  dvlip2  26308  dvcnvrelem2  26331  ftc1cn  26356  dvntaylp  26691  taylthlem1  26693  ulmdvlem3  26722  pserulm  26742  nodense  28042  mulsproplem13  28507  mulsproplem14  28508  onsbnd  28660  prlnghpg  29417  shsub2  31920  spanssoc  31944  shub2  31978  ococin  32003  ssjo  32042  chub2  32103  spanpr  32175  elnlfn  32523  mdslj1i  32914  mdslmd3i  32927  mdexchi  32930  chirredlem1  32985  atcvat3i  32991  mdsymlem1  32998  mdsymlem5  33002  imadifxp  33188  fnpreimac  33257  suppovss  33267  symgcom2  33638  pmtrcnelor  33645  cycpmco2f1  33678  0ringsubrg  33805  erlval  33812  1fldgenq  33877  elrspunidl  33971  drngmxidl  33994  drngmxidlr  33995  idlsrgmulrss1  34036  idlsrgmulrss2  34037  1arithidomlem2  34061  ply1dg3rt0irred  34109  resssra  34212  lsssra  34213  drgextlsp  34219  lvecdim0  34232  lbslsat  34241  dimkerim  34252  fedgmullem2  34255  fedgmul  34256  fldgenfldext  34293  fldextrspunlsplem  34298  fldextrspunlsp  34299  fldextrspunlem1  34300  fldextrspunfld  34301  fldextrspundgdvdslem  34305  fldextrspundgdvds  34306  algextdeglem3  34344  algextdeglem4  34345  qtophaus  34461  locfinreflem  34465  rspecbas  34490  zarclssn  34498  zarmxt1  34505  zarcmplem  34506  fsumcvg4  34575  esum2d  34718  omsmon  34923  omssubadd  34925  carsgclctun  34946  sitgclg  34967  eulerpartlemgf  35004  reprpmtf1o  35248  cvmscld  36017  cvmliftmolem1  36025  cvmlift2lem9  36055  cvmlift2lem11  36057  cvmlift3lem6  36068  nadddilem4  36952  opnregcld  37098  ivthALT  37103  neibastop2  37129  fnemeet1  37134  fnejoin1  37136  pibt2  38320  poimirlem11  38529  poimirlem12  38530  poimirlem30  38548  ftc1cnnc  38590  sstotbnd  38689  ssbnd  38702  heibor1lem  38723  heiborlem3  38727  heibor  38735  lsmsat  40045  lssats  40049  lcvexchlem3  40073  lsatcvat3  40089  lkrscss  40135  lkrpssN  40200  pmod1i  40885  pclbtwnN  40934  pclunN  40935  pclss2polN  40958  pcl0N  40959  sspmaplubN  40962  paddunN  40964  pnonsingN  40970  pclfinclN  40987  osumcllem4N  40996  dia2dimlem13  42113  dvhopellsm  42154  dvadiaN  42165  dicelval1stN  42225  dicelval2nd  42226  dihssxp  42289  dihvalrel  42316  dochsscl  42405  dihoml4  42414  dochnoncon  42428  dvh3dim3N  42486  lcfrlem2  42580  lcfrlem5  42583  lcfr  42622  lcdlsp  42658  mapdsn  42678  mapdlsm  42701  mapdpglem1  42709  mapdindp0  42756  hlhilocv  42994  primrootscoprbij  43132  rntrclfvOAI  43681  ismrcd1  43688  ismrcd2  43689  coeq0i  43743  hbtlem6  44115  iocinico  44198  omabs2  44318  naddwordnexlem4  44387  trclubNEW  44604  ntrk2imkb  45022  isotone1  45033  k0004ss3  45138  iccdifprioo  46497  limsupequzmptlem  46707  cncfuni  46865  cncfiooicclem1  46872  dvresntr  46897  itgsubsticclem  46954  fourierdlem42  47128  fourierdlem48  47133  fourierdlem49  47134  fourierdlem50  47135  qndenserrn  47278  prsal  47297  intsaluni  47308  sssalgen  47314  dfsalgen2  47320  sge0split  47388  ismeannd  47446  caragensspw  47488  caragendifcl  47493  carageniuncl  47502  caratheodorylem1  47505  hoicvrrex  47535  ovnssle  47540  ovn02  47547  ovnsubadd  47551  hoidmv1le  47573  ovnlecvr2  47589  ovncvr2  47590  isvonmbl  47617  vonmblss  47619  ovolval4lem2  47629  ovnovollem1  47635  ovnovollem2  47636  incsmf  47721  decsmf  47746  uspgropssxp  49211  mreuniss  49977  restcls2lem  49990  restcls2  49991  cnneiima  49994  imassc  50230