Theorem sseqtrd 3958

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 233	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  sseqtrrd  3959  sseqtrid  3964  3sstr3d  3976  uniintsn  4922  fssdmd  6680  oeeui  8535  nnaword2  8563  oaabs2  8582  naddword2  8625  erssxp  8664  fipwuni  9336  cantnflem3  9610  ficardun2  10122  ackbij1lem12  10150  ackbij1b  10158  fin1a2lem13  10332  winafp  10618  ioodisj  13433  reltrclfv  14977  prodss  15910  mrcssv  17578  mrcsscl  17584  mrcuni  17585  mressmrcd  17591  mreexexlem2d  17609  mreexexlem3d  17610  mreexfidimd  17614  subcss2  17808  resssetc  18057  funcsetcres2  18058  estrres  18103  poslubdg  18376  ipodrsfi  18503  acsmap2d  18519  mrelatlub  18526  mreclatBAD  18527  subsubmgm  18676  subsubm  18782  subsubg  19123  trivsubgd  19126  trivnsgd  19145  oppglsm  19615  subglsm  19646  lsmdisj  19654  gsumval3  19880  dprdres  20003  dprdss  20004  dprd2da  20017  dmdprdsplit2lem  20020  ablfac1b  20045  pgpfac1lem3  20052  subsubrng  20542  subsubrg  20577  rgspnval  20591  issubdrg  20759  islssd  20932  lspun  20984  lspssp  20985  lsslsp  21012  lsmssspx  21085  lspabs2  21120  lspabs3  21121  lspsolvlem  21142  lbsextlem3  21160  qsssubdrg  21408  obselocv  21710  lsslindf  21812  sraassa  21851  mplbas2  22025  gsumply1subr  22225  tgcl  22959  basgen  22978  tgfiss  22981  bastop1  22983  bastop2  22984  clsss2  23062  elcls3  23073  topssnei  23114  neiptopnei  23122  neitr  23170  restcls  23171  restlp  23173  ordtrest2  23194  iscncl  23259  cncls2  23263  cncls  23264  cnntr  23265  lmcls  23292  tgcmp  23391  cmpcld  23392  uncmp  23393  hauscmplem  23396  cmpfi  23398  clsconn  23420  2ndcsb  23439  2ndcctbss  23445  2ndcomap  23448  nllyrest  23476  1stckgenlem  23543  kgencn2  23547  kgen2cn  23549  ptbasfi  23571  txcld  23593  txcls  23594  txbasval  23596  neitx  23597  ptcld  23603  ptclsg  23605  txnlly  23627  hausdiag  23635  txkgen  23642  xkopt  23645  xkopjcn  23646  xkococnlem  23649  cnmpt1res  23666  cnmpt2res  23667  imasnopn  23680  imasncld  23681  imasncls  23682  qtopcld  23703  qtoprest  23707  qtopcmap  23709  kqcldsat  23723  kqreglem2  23732  kqnrmlem2  23734  hmeontr  23759  neifil  23870  fgtr  23880  trnei  23882  uffixfr  23913  uffix2  23914  uffixsn  23915  elflim  23961  flimclslem  23974  fclsopn  24004  fclscmpi  24019  fclscmp  24020  alexsubALTlem3  24039  alexsubALT  24041  ptcmplem3  24044  subgntr  24097  opnsubg  24098  clssubg  24099  clsnsg  24100  cldsubg  24101  tgpconncompeqg  24102  snclseqg  24106  tsmsgsum  24129  tsmsid  24130  tgptsmscld  24141  ustssco  24205  utop2nei  24240  utop3cls  24241  utopreg  24242  cnextucn  24292  ressprdsds  24361  lpbl  24493  met2ndci  24512  prdsxmslem2  24519  metustexhalf  24546  psmetutop  24557  tgioo  24786  metdstri  24842  metdseq0  24845  xlebnum  24957  clsocv  25242  metelcls  25297  metsscmetcld  25307  cmetss  25308  relcmpcmet  25310  cmpcmet  25311  minveclem4a  25422  uniioovol  25571  uniioombllem3  25577  limcres  25878  dvbss  25893  perfdvf  25895  dvreslem  25901  dvres2lem  25902  dvmptresicc  25908  dvcnp2  25912  dvaddbr  25930  dvmulbr  25931  dvcmulf  25937  dvcj  25942  dvnfre  25944  dvmptres2  25954  dvmptcmul  25956  dvmptntr  25963  dvlip2  25987  dvcnvrelem2  26010  ftc1cn  26035  dvntaylp  26361  taylthlem1  26363  ulmdvlem3  26392  pserulm  26412  nodense  27681  mulsproplem13  28145  mulsproplem14  28146  onsbnd  28298  shsub2  31421  spanssoc  31445  shub2  31479  ococin  31504  ssjo  31543  chub2  31604  spanpr  31676  elnlfn  32024  mdslj1i  32415  mdslmd3i  32428  mdexchi  32431  chirredlem1  32486  atcvat3i  32492  mdsymlem1  32499  mdsymlem5  32503  imadifxp  32697  fnpreimac  32769  suppovss  32780  symgcom2  33172  pmtrcnelor  33179  cycpmco2f1  33212  0ringsubrg  33339  erlval  33346  1fldgenq  33413  0ringidl  33511  elrspunidl  33518  0ringprmidl  33539  drngmxidl  33567  drngmxidlr  33568  idlsrgmulrss1  33601  idlsrgmulrss2  33602  1arithidomlem2  33626  ply1dg3rt0irred  33674  resssra  33778  lsssra  33779  drgextlsp  33785  lvecdim0  33798  lbslsat  33807  dimkerim  33818  fedgmullem2  33821  fedgmul  33822  fldgenfldext  33859  fldextrspunlsplem  33864  fldextrspunlsp  33865  fldextrspunlem1  33866  fldextrspunfld  33867  fldextrspundgdvdslem  33871  fldextrspundgdvds  33872  algextdeglem3  33910  algextdeglem4  33911  qtophaus  34027  locfinreflem  34031  rspecbas  34056  zarclssn  34064  zarmxt1  34071  zarcmplem  34072  fsumcvg4  34141  esum2d  34284  omsmon  34489  omssubadd  34491  carsgclctun  34512  sitgclg  34533  eulerpartlemgf  34570  reprpmtf1o  34817  cvmscld  35508  cvmliftmolem1  35516  cvmlift2lem9  35546  cvmlift2lem11  35548  cvmlift3lem6  35559  opnregcld  36565  ivthALT  36570  neibastop2  36596  fnemeet1  36601  fnejoin1  36603  pibt2  37786  poimirlem11  38005  poimirlem12  38006  poimirlem30  38024  ftc1cnnc  38066  sstotbnd  38149  ssbnd  38162  heibor1lem  38183  heiborlem3  38187  heibor  38195  lsmsat  39507  lssats  39511  lcvexchlem3  39535  lsatcvat3  39551  lkrscss  39597  lkrpssN  39662  pmod1i  40347  pclbtwnN  40396  pclunN  40397  pclss2polN  40420  pcl0N  40421  sspmaplubN  40424  paddunN  40426  pnonsingN  40432  pclfinclN  40449  osumcllem4N  40458  dia2dimlem13  41575  dvhopellsm  41616  dvadiaN  41627  dicelval1stN  41687  dicelval2nd  41688  dihssxp  41751  dihvalrel  41778  dochsscl  41867  dihoml4  41876  dochnoncon  41890  dvh3dim3N  41948  lcfrlem2  42042  lcfrlem5  42045  lcfr  42084  lcdlsp  42120  mapdsn  42140  mapdlsm  42163  mapdpglem1  42171  mapdindp0  42218  hlhilocv  42456  primrootscoprbij  42594  rntrclfvOAI  43147  ismrcd1  43154  ismrcd2  43155  coeq0i  43209  hbtlem6  43581  iocinico  43664  omabs2  43784  naddwordnexlem4  43853  trclubNEW  44070  ntrk2imkb  44488  isotone1  44499  k0004ss3  44604  iccdifprioo  45968  limsupequzmptlem  46178  cncfuni  46336  cncfiooicclem1  46343  dvresntr  46368  itgsubsticclem  46425  fourierdlem42  46599  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  qndenserrn  46749  prsal  46768  intsaluni  46779  sssalgen  46785  dfsalgen2  46791  sge0split  46859  ismeannd  46917  caragensspw  46959  caragendifcl  46964  carageniuncl  46973  caratheodorylem1  46976  hoicvrrex  47006  ovnssle  47011  ovn02  47018  ovnsubadd  47022  hoidmv1le  47044  ovnlecvr2  47060  ovncvr2  47061  isvonmbl  47088  vonmblss  47090  ovolval4lem2  47100  ovnovollem1  47106  ovnovollem2  47107  incsmf  47192  decsmf  47217  uspgropssxp  48642  mreuniss  49397  restcls2lem  49410  restcls2  49411  cnneiima  49414  imassc  49650