Theorem sseq1 3919

Description: Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

Ref	Expression
sseq1	⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Proof of Theorem sseq1

Step	Hyp	Ref	Expression
1		eqss 3909	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3901	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 485	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3901	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 215	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 220	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ⊆ wss 3860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877

This theorem is referenced by:  sseq12  3921  sseq1i  3922  sseq1d  3925  nssne2  3955  psseq1  3995  uneqdifeq  4389  sbss  4418  pwjust  4498  elpwg  4500  elpwOLD  4503  elpwgOLD  4504  pwpw0  4706  sssn  4719  ssunsn2  4720  pwsnOLD  4794  unimax  4839  trss  5150  al0ssb  5181  sseliALT  5182  elssabg  5209  intabs  5215  nnullss  5325  exss  5326  fri  5489  releq  5624  iss  5879  relcnvtrg  6100  fununi  6414  ssimaex  6741  isofrlem  7092  onssmin  7516  tfis  7573  tfisi  7577  funcnvuni  7646  ffoss  7656  f1oweALT  7682  frxp  7830  wfrlem1  7969  wfrlem4  7973  wfrlem15  7984  tfrlem1  8027  oawordeu  8196  qsss  8373  boxcutc  8528  sbthlem2  8655  sbth  8664  php  8728  findcard2d  8742  ssfi  8747  isinf  8774  unbnn2  8813  domunfican  8829  fiint  8833  finsschain  8869  indexfi  8870  dffi3  8933  hartogslem1  9044  cantnfval2  9170  cantnfle  9172  cantnflem1  9190  tz9.1  9209  setind  9214  tcvalg  9218  scott0  9353  bnd2  9360  carduni  9448  cardaleph  9554  alephinit  9560  aceq3lem  9585  dfac12lem3  9610  infmap2  9683  cflem  9711  cflm  9715  cflecard  9718  cfeq0  9721  cfsuc  9722  cfflb  9724  cfslb  9731  cfslb2n  9733  coftr  9738  fin23lem13  9797  fin23lem16  9800  fin23lem19  9801  fin23lem29  9806  fin1a2lem13  9877  itunitc  9886  domtriomlem  9907  axdc3lem2  9916  zorn2lem7  9967  zornn0g  9970  fpwwe2lem4  10099  pwfseqlem4a  10126  pwfseqlem4  10127  wunfi  10186  wunex2  10203  wuncval  10207  rankcf  10242  tskuni  10248  axgroth6  10293  axgroth3  10296  axgroth4  10297  fzoss1  13118  fsuppmapnn0fiubex  13414  hashf1lem2  13871  cleq1lem  14394  rtrclreclem4  14473  sumeq1  15098  fsumcvg3  15139  fsum2d  15179  fsumabs  15209  fsumrlim  15219  fsumo1  15220  fsumiun  15229  prodeq1f  15315  fprod2d  15388  lcmfunsnlem  16042  coprmprod  16062  vdwmc  16374  prmgaplem3  16449  prmgaplem4  16450  restsspw  16768  ismred2  16937  mrcval  16944  mrcuni  16955  acsfn  16993  isssc  17154  drsdirfi  17619  ipodrsima  17846  cntzssv  18530  pmtrfrn  18658  pmtrrn2  18660  pmtrdifellem1  18676  pmtrdifellem2  18677  sylow2alem2  18815  sylow2a  18816  efgval  18915  gsumzaddlem  19114  ablfac1eulem  19267  lspval  19820  lspindpi  19977  znf1o  20324  zntoslem  20329  aspval  20640  mplsubglem  20769  mpllsslem  20770  mplcoe1  20802  mplcoe5  20805  mdetunilem9  21325  uniopn  21602  fiinopn  21606  fiinbas  21657  baspartn  21659  eltg2  21663  eltg3  21667  topbas  21677  pptbas  21713  clsval  21742  neiint  21809  neips  21818  opnneissb  21819  opnssneib  21820  innei  21830  neiptoptop  21836  neiptopnei  21837  restbas  21863  restcld  21877  neitr  21885  restcls  21886  restntr  21887  cnpdis  21998  cmpsublem  22104  cmpsub  22105  fiuncmp  22109  unconn  22134  1stcfb  22150  2ndc1stc  22156  1stcrest  22158  2ndcctbss  22160  2ndcomap  22163  dis2ndc  22165  lly1stc  22201  refssex  22216  refun0  22220  llycmpkgen2  22255  txbas  22272  eltx  22273  ptuni2  22281  neitx  22312  ptpjopn  22317  ptcld  22318  txlm  22353  tx1stc  22355  txkgen  22357  xkopt  22360  xkococnlem  22364  ptcmpfi  22518  fbssfi  22542  opnfbas  22547  isfil2  22561  isfildlem  22562  snfil  22569  fsubbas  22572  ssfg  22577  fgss2  22579  fgcl  22583  fbasrn  22589  fgtr  22595  ufli  22619  uffix  22626  rnelfmlem  22657  fclscf  22730  alexsublem  22749  alexsubALTlem2  22753  alexsubALTlem3  22754  alexsubALTlem4  22755  alexsubALT  22756  tmdgsum2  22801  subgntr  22812  opnsubg  22813  qustgpopn  22825  tsmsfbas  22833  tsmsgsum  22844  tsmsres  22849  tsmsf1o  22850  tsmsxplem1  22858  tsmsxp  22860  isust  22909  ustssel  22911  ustincl  22913  ustdiag  22914  ustinvel  22915  ustexhalf  22916  ustexsym  22921  ust0  22925  restutop  22943  ustuqtop4  22950  utopsnneiplem  22953  blssexps  23133  blssex  23134  neibl  23208  blcld  23212  met1stc  23228  met2ndci  23229  metrest  23231  prdsxmslem2  23236  metustfbas  23264  cfilucfil  23266  metuel2  23272  metustbl  23273  restmetu  23277  dscopn  23280  isngp2  23304  tgioo  23502  tgqioo  23506  zdis  23522  xrge0tsms  23540  fsumcn  23576  volivth  24312  vitalilem2  24314  itgfsum  24531  limcun  24599  recnprss  24608  dvmptfsum  24679  ftc1a  24741  plyssc  24901  efopn  25353  jensen  25678  tglnunirn  26446  lpvtx  26965  umgredgprv  27004  usgredgprvALT  27089  issubgr2  27166  subgrprop2  27168  egrsubgr  27171  0uhgrsubgr  27173  frcond3  28158  hhsssh  29156  shintcl  29217  chintcl  29219  spanval  29220  omlsi  29291  pjoml  29323  chnlen0  29331  chsscon3  29387  chlejb1  29399  chnle  29401  spanun  29432  h1datom  29469  cmbr4i  29488  pjoml2  29498  pjoml3  29499  lecm  29504  osumcor2i  29531  osum  29532  spansncv  29540  pjcjt2  29579  pjopyth  29607  hstel2  30106  stj  30122  stcltr1i  30161  mdi  30182  mdbr3  30184  mdbr4  30185  dmdbr  30186  dmdmd  30187  dmdbr5  30195  mdsl1i  30208  mdslmd1lem3  30214  mdslmd1lem4  30215  mdslmd1i  30216  csmdsymi  30221  atss  30233  atom1d  30240  superpos  30241  chcv1  30242  shatomici  30245  shatomistici  30248  hatomistici  30249  chrelat2  30257  chirredi  30281  atcvat4i  30284  mdsymlem2  30291  mdsymlem6  30295  dmdbr6ati  30310  dmdbr7ati  30311  xrge0tsmsd  30847  gsumle  30880  gsumvsca1  31009  gsumvsca2  31010  prmidl  31140  ismxidl  31159  zarcls1  31344  zarclsun  31345  zarclsiin  31346  zarclsint  31347  zarclssn  31348  zartop  31351  zartopon  31352  zart0  31354  zarmxt1  31355  zarcmp  31357  rhmpreimacnlem  31359  rhmpreimacn  31360  tpr2rico  31387  issiga  31603  isrnsiga  31604  sigagenval  31631  measiuns  31708  dya2icoseg  31767  dya2iocnrect  31771  dya2iocuni  31773  carsgmon  31804  carsgsigalem  31805  carsgclctunlem2  31809  carsgclctun  31811  pmeasmono  31814  pmeasadd  31815  bnj517  32389  bnj1118  32488  bnj1145  32497  bnj1154  32503  bnj1452  32556  bnj1498  32565  pthhashvtx  32609  kur14lem1  32688  cvmopnlem  32760  dfon2lem3  33281  dfon2lem7  33285  frmin  33338  frxp2  33350  frxp3  33356  frrlem1  33389  frrlem13  33401  brsslt  33569  madef  33626  brsset  33766  fness  34113  fneref  34114  fnessref  34121  neibastop2lem  34124  topmeet  34128  fnejoin2  34133  tailfb  34141  filnetlem4  34145  onsucsuccmpi  34207  bj-snglss  34713  bj-restpw  34813  bj-imdirco  34911  dissneqlem  35063  relowlssretop  35086  relowlpssretop  35087  ctbssinf  35129  pibt2  35140  matunitlindflem1  35359  ptrecube  35363  poimirlem29  35392  mblfinlem2  35401  mblfinlem3  35402  mblfinlem4  35403  ismblfin  35404  ovoliunnfl  35405  voliunnfl  35407  volsupnfl  35408  indexa  35477  indexdom  35478  neificl  35497  istotbnd3  35515  sstotbnd2  35518  sstotbnd  35519  equivtotbnd  35522  ssbnd  35532  heiborlem1  35555  heiborlem6  35560  heiborlem8  35562  heiborlem10  35564  unichnidl  35775  pridl  35781  ismaxidl  35784  igenval  35805  igenval2  35810  ispridlc  35814  relcnveq3  36044  iss2  36067  elrelscnveq3  36197  brssr  36207  lsmsat  36610  lssatomic  36613  lssats  36614  lsat0cv  36635  lcvexchlem4  36639  lcvexchlem5  36640  lsatcvatlem  36651  l1cvpat  36656  ispsubsp  37347  linepsubN  37354  pclvalN  37492  ispsubclN  37539  ispsubcl2N  37549  pclfinclN  37552  diaelrnN  38647  docavalN  38725  dochval  38953  dvh4dimat  39040  dochexmidlem1  39062  lpolconN  39089  mapdordlem2  39239  ismrcd1  40040  ismrcd2  40041  ismrc  40043  mzpcompact2lem  40093  aomclem6  40404  hbtlem6  40474  rgspnval  40513  ssficl  40669  ssuncl  40670  ssdifcl  40671  sssymdifcl  40672  elmapintrab  40677  clcnvlem  40724  iunrelexpmin1  40810  iunrelexpmin2  40814  clsk3nimkb  41144  clsk1indlem1  41149  isotone1  41152  isotone2  41153  ntrclsiso  41171  gneispace  41238  gneispacess2  41250  onfrALTlem5  41649  onfrALTlem5VD  41992  islptre  42655  dvmptconst  42951  dvmptidg  42953  dvmulcncf  42961  dvdivcncf  42963  dvmptfprod  42981  stoweidlem51  43087  stoweidlem52  43088  fourierdlem103  43245  fourierdlem104  43246  ioorrnopnlem  43340  ioorrnopnxrlem  43342  salgenval  43357  ovnval2  43578  ovncvrrp  43597  ovnsubaddlem1  43603  ovnsubadd  43605  ovncvr2  43644  hspmbl  43662  elsetpreimafvssdm  44299  uspgrsprfo  44771  sepfsepc  45639  setrec1lem1  45681  setrec1lem4  45684  setrec2fun  45686  elsetrecslem  45692  elpglem2  45705