Theorem sseq1 4006

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 3996	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3988	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 483	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3988	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 482	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 211	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 216	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ⊆ wss 3947

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3954  df-ss 3964

This theorem is referenced by:  sseq12  4008  sseq1i  4009  sseq1d  4012  nssne2  4044  psseq1  4086  uneqdifeq  4491  sbss  4521  pwjust  4602  elpwg  4604  pwpw0  4815  sssn  4828  ssunsn2  4829  pwsnOLD  4900  unimax  4947  trss  5275  al0ssb  5307  sseliALT  5308  elssabg  5335  intabs  5341  vpwex  5374  nnullss  5461  exss  5462  friOLD  5636  releq  5774  iss  6033  relcnvtrg  6262  fununi  6620  ssimaex  6972  isofrlem  7332  onssmin  7775  tfis  7839  tfisi  7843  funcnvuni  7917  ffoss  7927  f1oweALT  7954  frxp  8107  frxp2  8125  frrlem1  8266  frrlem13  8278  wfrlem1OLD  8303  wfrlem4OLD  8307  wfrlem15OLD  8318  tfrlem1  8371  oawordeu  8551  coflton  8666  cofon1  8667  cofon2  8668  naddunif  8688  qsss  8768  boxcutc  8931  sbthlem2  9080  sbth  9089  findcard2d  9162  ssfi  9169  sbthfi  9198  php  9206  phpOLD  9218  isinf  9256  isinfOLD  9257  unbnn2  9296  domunfican  9316  fiint  9320  finsschain  9355  indexfi  9356  dffi3  9422  hartogslem1  9533  cantnfval2  9660  cantnfle  9662  cantnflem1  9680  tz9.1  9720  setind  9725  tcvalg  9729  frmin  9740  scott0  9877  bnd2  9884  carduni  9972  cardaleph  10080  alephinit  10086  aceq3lem  10111  dfac12lem3  10136  infmap2  10209  cflem  10237  cflm  10241  cflecard  10244  cfeq0  10247  cfsuc  10248  cfflb  10250  cfslb  10257  cfslb2n  10259  coftr  10264  fin23lem13  10323  fin23lem16  10326  fin23lem19  10327  fin23lem29  10332  fin1a2lem13  10403  itunitc  10412  domtriomlem  10433  axdc3lem2  10442  zorn2lem7  10493  zornn0g  10496  fpwwe2lem4  10625  pwfseqlem4a  10652  pwfseqlem4  10653  wunfi  10712  wunex2  10729  wuncval  10733  rankcf  10768  tskuni  10774  axgroth6  10819  axgroth3  10822  axgroth4  10823  fzoss1  13655  fsuppmapnn0fiubex  13953  hashf1lem2  14413  cleq1lem  14925  rtrclreclem4  15004  sumeq1  15631  fsumcvg3  15671  fsum2d  15713  fsumabs  15743  fsumrlim  15753  fsumo1  15754  fsumiun  15763  prodeq1f  15848  fprod2d  15921  lcmfunsnlem  16574  coprmprod  16594  vdwmc  16907  prmgaplem3  16982  prmgaplem4  16983  restsspw  17373  ismred2  17543  mrcval  17550  mrcuni  17561  acsfn  17599  isssc  17763  drsdirfi  18254  ipodrsima  18490  cntzssv  19186  pmtrfrn  19319  pmtrrn2  19321  pmtrdifellem1  19337  pmtrdifellem2  19338  sylow2alem2  19479  sylow2a  19480  efgval  19578  gsumzaddlem  19781  ablfac1eulem  19934  lspval  20574  lspindpi  20733  znf1o  21091  zntoslem  21096  aspval  21409  mplsubglem  21540  mpllsslem  21541  mplcoe1  21574  mplcoe5  21577  mdetunilem9  22104  uniopn  22381  fiinopn  22385  fiinbas  22437  baspartn  22439  eltg2  22443  eltg3  22447  topbas  22457  pptbas  22493  clsval  22523  neiint  22590  neips  22599  opnneissb  22600  opnssneib  22601  innei  22611  neiptoptop  22617  neiptopnei  22618  restbas  22644  restcld  22658  neitr  22666  restcls  22667  restntr  22668  cnpdis  22779  cmpsublem  22885  cmpsub  22886  fiuncmp  22890  unconn  22915  1stcfb  22931  2ndc1stc  22937  1stcrest  22939  2ndcctbss  22941  2ndcomap  22944  dis2ndc  22946  lly1stc  22982  refssex  22997  refun0  23001  llycmpkgen2  23036  txbas  23053  eltx  23054  ptuni2  23062  neitx  23093  ptpjopn  23098  ptcld  23099  txlm  23134  tx1stc  23136  txkgen  23138  xkopt  23141  xkococnlem  23145  ptcmpfi  23299  fbssfi  23323  opnfbas  23328  isfil2  23342  isfildlem  23343  snfil  23350  fsubbas  23353  ssfg  23358  fgss2  23360  fgcl  23364  fbasrn  23370  fgtr  23376  ufli  23400  uffix  23407  rnelfmlem  23438  fclscf  23511  alexsublem  23530  alexsubALTlem2  23534  alexsubALTlem3  23535  alexsubALTlem4  23536  alexsubALT  23537  tmdgsum2  23582  subgntr  23593  opnsubg  23594  qustgpopn  23606  tsmsfbas  23614  tsmsgsum  23625  tsmsres  23630  tsmsf1o  23631  tsmsxplem1  23639  tsmsxp  23641  isust  23690  ustssel  23692  ustincl  23694  ustdiag  23695  ustinvel  23696  ustexhalf  23697  ustexsym  23702  ust0  23706  restutop  23724  ustuqtop4  23731  utopsnneiplem  23734  blssexps  23914  blssex  23915  neibl  23992  blcld  23996  met1stc  24012  met2ndci  24013  metrest  24015  prdsxmslem2  24020  metustfbas  24048  cfilucfil  24050  metuel2  24056  metustbl  24057  restmetu  24061  dscopn  24064  isngp2  24088  tgioo  24294  tgqioo  24298  zdis  24314  xrge0tsms  24332  fsumcn  24368  volivth  25106  vitalilem2  25108  itgfsum  25326  limcun  25394  recnprss  25403  dvmptfsum  25474  ftc1a  25536  plyssc  25696  efopn  26148  jensen  26473  brsslt  27267  madef  27331  tglnunirn  27779  lpvtx  28308  umgredgprv  28347  usgredgprvALT  28432  issubgr2  28509  subgrprop2  28511  egrsubgr  28514  0uhgrsubgr  28516  frcond3  29502  hhsssh  30500  shintcl  30561  chintcl  30563  spanval  30564  omlsi  30635  pjoml  30667  chnlen0  30675  chsscon3  30731  chlejb1  30743  chnle  30745  spanun  30776  h1datom  30813  cmbr4i  30832  pjoml2  30842  pjoml3  30843  lecm  30848  osumcor2i  30875  osum  30876  spansncv  30884  pjcjt2  30923  pjopyth  30951  hstel2  31450  stj  31466  stcltr1i  31505  mdi  31526  mdbr3  31528  mdbr4  31529  dmdbr  31530  dmdmd  31531  dmdbr5  31539  mdsl1i  31552  mdslmd1lem3  31558  mdslmd1lem4  31559  mdslmd1i  31560  csmdsymi  31565  atss  31577  atom1d  31584  superpos  31585  chcv1  31586  shatomici  31589  shatomistici  31592  hatomistici  31593  chrelat2  31601  chirredi  31625  atcvat4i  31628  mdsymlem2  31635  mdsymlem6  31639  dmdbr6ati  31654  dmdbr7ati  31655  xrge0tsmsd  32187  gsumle  32220  gsumvsca1  32349  gsumvsca2  32350  prmidl  32516  ismxidl  32536  zarcls1  32787  zarclsun  32788  zarclsiin  32789  zarclsint  32790  zarclssn  32791  zartop  32794  zartopon  32795  zart0  32797  zarmxt1  32798  zarcmp  32800  rhmpreimacnlem  32802  rhmpreimacn  32803  tpr2rico  32830  issiga  33048  isrnsiga  33049  sigagenval  33076  measiuns  33153  dya2icoseg  33214  dya2iocnrect  33218  dya2iocuni  33220  carsgmon  33251  carsgsigalem  33252  carsgclctunlem2  33256  carsgclctun  33258  pmeasmono  33261  pmeasadd  33262  bnj517  33834  bnj1118  33933  bnj1145  33942  bnj1154  33948  bnj1452  34001  bnj1498  34010  fineqvpow  34034  fineqvac  34035  fineqvacALT  34036  pthhashvtx  34056  kur14lem1  34135  cvmopnlem  34207  dfon2lem3  34695  dfon2lem7  34699  brsset  34799  fness  35172  fneref  35173  fnessref  35180  neibastop2lem  35183  topmeet  35187  fnejoin2  35192  tailfb  35200  filnetlem4  35204  onsucsuccmpi  35266  bj-snglss  35789  bj-elpwgALT  35873  bj-restpw  35911  bj-imdirco  36009  dissneqlem  36159  relowlssretop  36182  relowlpssretop  36183  ctbssinf  36225  pibt2  36236  matunitlindflem1  36422  ptrecube  36426  poimirlem29  36455  mblfinlem2  36464  mblfinlem3  36465  mblfinlem4  36466  ismblfin  36467  ovoliunnfl  36468  voliunnfl  36470  volsupnfl  36471  indexa  36539  indexdom  36540  neificl  36559  istotbnd3  36577  sstotbnd2  36580  sstotbnd  36581  equivtotbnd  36584  ssbnd  36594  heiborlem1  36617  heiborlem6  36622  heiborlem8  36624  heiborlem10  36626  unichnidl  36837  pridl  36843  ismaxidl  36846  igenval  36867  igenval2  36872  ispridlc  36876  relcnveq3  37128  iss2  37151  elrelscnveq3  37299  brssr  37309  lsmsat  37816  lssatomic  37819  lssats  37820  lsat0cv  37841  lcvexchlem4  37845  lcvexchlem5  37846  lsatcvatlem  37857  l1cvpat  37862  ispsubsp  38554  linepsubN  38561  pclvalN  38699  ispsubclN  38746  ispsubcl2N  38756  pclfinclN  38759  diaelrnN  39854  docavalN  39932  dochval  40160  dvh4dimat  40247  dochexmidlem1  40269  lpolconN  40296  mapdordlem2  40446  eqresfnbd  41003  ismrcd1  41369  ismrcd2  41370  ismrc  41372  mzpcompact2lem  41422  aomclem6  41734  hbtlem6  41804  rgspnval  41843  onintunirab  41909  rp-brsslt  42107  ssficl  42253  ssuncl  42254  ssdifcl  42255  sssymdifcl  42256  elmapintrab  42260  clcnvlem  42307  iunrelexpmin1  42392  iunrelexpmin2  42396  clsk3nimkb  42724  clsk1indlem1  42729  isotone1  42732  isotone2  42733  ntrclsiso  42751  gneispace  42818  gneispacess2  42830  onfrALTlem5  43236  onfrALTlem5VD  43579  islptre  44270  dvmptconst  44566  dvmptidg  44568  dvmulcncf  44576  dvdivcncf  44578  dvmptfprod  44596  stoweidlem51  44702  stoweidlem52  44703  fourierdlem103  44860  fourierdlem104  44861  ioorrnopnlem  44955  ioorrnopnxrlem  44957  salgenval  44972  ovnval2  45196  ovncvrrp  45215  ovnsubaddlem1  45221  ovnsubadd  45223  ovncvr2  45262  hspmbl  45280  elsetpreimafvssdm  45989  uspgrsprfo  46461  unilbss  47404  sepfsepc  47462  unilbeu  47512  ipolubdm  47514  ipoglbdm  47517  setrec1lem1  47634  setrec1lem4  47637  setrec2fun  47639  elsetrecslem  47646  elpglem2  47659