Theorem sseq1 3963

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 3953	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3945	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3945	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	2, 3	anbiim 652	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
5	4	ancoms 463	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
6	1, 5	sylbi 220	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  sseq12  3965  sseq1i  3966  sseq1d  3969  nssne2  4001  psseq1  4045  vvin  4367  uneqdifeq  4454  sbss  4482  pwjust  4564  elpwg  4566  pwpw0  4780  sssn  4793  ssunsn2  4794  unimax  4911  trss  5229  al0ssb  5272  sseliALT  5273  elssabg  5315  intabs  5321  vpwex  5350  nnullss  5445  exss  5446  releq  5765  iss  6039  relcnvtrg  6270  fununi  6613  ssimaex  6968  isofrlem  7340  onssmin  7792  tfis  7852  tfisi  7856  funcnvuni  7930  ffoss  7944  f1oweALT  7970  frxp  8123  frxp2  8141  frrlem1  8284  frrlem13  8296  tfrlem1  8363  oawordeu  8541  coflton  8658  cofon1  8659  cofon2  8660  naddunif  8681  qsss  8774  boxcutc  8940  sbthlem2  9077  sbth  9086  findcard2d  9152  ssfi  9158  sbthfi  9184  php  9192  isinf  9226  unbnn2  9258  domunfican  9282  fiint  9287  finsschain  9317  indexfi  9318  dffi3  9392  hartogslem1  9505  cantnfval2  9639  cantnfle  9641  cantnflem1  9659  tz9.1  9699  tcvalg  9706  setind  9717  frmin  9722  scott0  9861  bnd2  9880  carduni  9968  cardaleph  10074  alephinit  10080  aceq3lem  10105  dfac12lem3  10130  infmap2  10201  cflem  10229  cflemOLD  10230  cflm  10234  cflecard  10237  cfeq0  10241  cfsuc  10242  cfflb  10244  cfslb  10251  cfslb2n  10253  coftr  10258  fin23lem13  10317  fin23lem16  10320  fin23lem19  10321  fin23lem29  10326  fin1a2lem13  10397  itunitc  10406  domtriomlem  10427  axdc3lem2  10436  zorn2lem7  10487  zornn0g  10490  pwfseqlem4a  10647  pwfseqlem4  10648  wunfi  10707  wunex2  10724  wuncval  10728  rankcf  10763  tskuni  10769  axgroth6  10814  axgroth3  10817  axgroth4  10818  fzoss1  13717  fsuppmapnn0fiubex  14030  hashf1lem2  14495  cleq1lem  15021  rtrclreclem4  15100  sumeq1  15742  fsumcvg3  15782  fsum2d  15824  fsumabs  15855  fsumrlim  15865  fsumo1  15866  fsumiun  15875  prodeq1f  15962  prodeq1  15963  fprod2d  16037  lcmfunsnlem  16700  coprmprod  16720  vdwmc  17039  prmgaplem3  17114  prmgaplem4  17115  restsspw  17485  ismred2  17656  mrcval  17667  mrcuni  17678  acsfn  17716  isssc  17878  drsdirfi  18362  ipodrsima  18598  cntzssv  19399  pmtrfrn  19529  pmtrrn2  19531  pmtrdifellem1  19547  pmtrdifellem2  19548  sylow2alem2  19689  sylow2a  19690  efgval  19788  gsumzaddlem  19992  ablfac1eulem  20145  gsumle  20216  rgspnval  20698  lspval  21077  lspindpi  21237  unichnlidl  21343  rspprop  21351  prmidl  21446  znf1o  21682  zntoslem  21687  aspval  22003  mplsubglem  22129  mpllsslem  22130  mplcoe1  22169  mplcoe5  22172  mdetunilem9  22758  uniopn  23035  fiinopn  23039  fiinbas  23090  baspartn  23092  eltg2  23096  eltg3  23100  topbas  23110  pptbas  23146  clsval  23175  neiint  23242  neips  23251  opnneissb  23252  opnssneib  23253  innei  23263  neiptoptop  23269  neiptopnei  23270  restbas  23296  restcld  23310  neitr  23318  restcls  23319  restntr  23320  cnpdis  23431  cmpsublem  23537  cmpsub  23538  fiuncmp  23542  unconn  23567  1stcfb  23583  2ndc1stc  23589  1stcrest  23591  2ndcctbss  23593  2ndcomap  23596  dis2ndc  23598  lly1stc  23634  refssex  23649  refun0  23653  llycmpkgen2  23688  txbas  23705  eltx  23706  ptuni2  23714  neitx  23745  ptpjopn  23750  ptcld  23751  txlm  23786  tx1stc  23788  txkgen  23790  xkopt  23793  xkococnlem  23797  ptcmpfi  23951  fbssfi  23975  opnfbas  23980  isfil2  23994  isfildlem  23995  snfil  24002  fsubbas  24005  ssfg  24010  fgss2  24012  fgcl  24016  fbasrn  24022  fgtr  24028  ufli  24052  uffix  24059  rnelfmlem  24090  fclscf  24163  alexsublem  24182  alexsubALTlem2  24186  alexsubALTlem3  24187  alexsubALTlem4  24188  alexsubALT  24189  tmdgsum2  24234  subgntr  24245  opnsubg  24246  qustgpopn  24258  tsmsfbas  24266  tsmsgsum  24277  tsmsres  24282  tsmsf1o  24283  tsmsxplem1  24291  tsmsxp  24293  isust  24342  ustssel  24344  ustincl  24346  ustdiag  24347  ustinvel  24348  ustexhalf  24349  ustexsym  24354  ust0  24358  restutop  24375  ustuqtop4  24382  utopsnneiplem  24385  blssexps  24564  blssex  24565  neibl  24639  blcld  24643  met1stc  24659  met2ndci  24660  metrest  24662  prdsxmslem2  24667  metustfbas  24695  cfilucfil  24697  metuel2  24703  metustbl  24704  restmetu  24708  dscopn  24711  isngp2  24735  tgioo  24934  tgqioo  24938  zdis  24955  xrge0tsms  24973  fsumcn  25010  volivth  25747  vitalilem2  25749  itgfsum  25967  limcun  26035  recnprss  26044  dvmptfsum  26115  ftc1a  26177  plyssc  26338  efopn  26801  jensen  27131  brslts  27933  madef  28007  tglnunirn  28795  brprlng  29166  lpvtx  29396  umgredgprv  29435  usgredgprvALT  29523  issubgr2  29600  subgrprop2  29602  egrsubgr  29605  0uhgrsubgr  29607  frcond3  30598  hhsssh  31599  shintcl  31660  chintcl  31662  spanval  31663  omlsi  31734  pjoml  31766  chnlen0  31774  chsscon3  31830  chlejb1  31842  chnle  31844  spanun  31875  h1datom  31912  cmbr4i  31931  pjoml2  31941  pjoml3  31942  lecm  31947  osumcor2i  31974  osum  31975  spansncv  31983  pjcjt2  32022  pjopyth  32050  hstel2  32549  stj  32565  stcltr1i  32604  mdi  32625  mdbr3  32627  mdbr4  32628  dmdbr  32629  dmdmd  32630  dmdbr5  32638  mdsl1i  32651  mdslmd1lem3  32657  mdslmd1lem4  32658  mdslmd1i  32659  csmdsymi  32664  atss  32676  atom1d  32683  superpos  32684  chcv1  32685  shatomici  32688  shatomistici  32691  hatomistici  32692  chrelat2  32700  chirredi  32724  atcvat4i  32727  mdsymlem2  32734  mdsymlem6  32738  dmdbr6ati  32753  dmdbr7ati  32754  xrge0tsmsd  33371  gsumvsca1  33524  gsumvsca2  33525  ismxidl  33723  constrfiss  34119  zarcls1  34237  zarclsun  34238  zarclsiin  34239  zarclsint  34240  zarclssn  34241  zartop  34244  zartopon  34245  zart0  34247  zarmxt1  34248  zarcmp  34250  rhmpreimacnlem  34252  rhmpreimacn  34253  tpr2rico  34280  issiga  34480  isrnsiga  34481  sigagenval  34508  measiuns  34585  dya2icoseg  34645  dya2iocnrect  34649  dya2iocuni  34651  carsgmon  34682  carsgsigalem  34683  carsgclctunlem2  34687  carsgclctun  34689  pmeasmono  34692  pmeasadd  34693  bnj517  35251  bnj1118  35350  bnj1145  35359  bnj1154  35365  bnj1452  35418  bnj1498  35427  rankscottu  35501  fineqvpow  35506  fineqvac  35507  fineqvacALT  35508  setindregs  35521  tz9.1regs  35525  fineqvr1ombregs  35529  rankkardu  35562  vonf1wev  35570  vonf1owevOLD  35572  pthhashvtx  35598  kur14lem1  35676  cvmopnlem  35748  dfon2lem3  36253  dfon2lem7  36257  brsset  36357  fness  36838  fneref  36839  fnessref  36846  neibastop2lem  36849  topmeet  36853  fnejoin2  36858  tailfb  36866  filnetlem4  36870  onsucsuccmpi  36932  ttcwf2  37014  ttcexg  37021  bj-snglss  37584  bj-elpwgALT  37668  bj-restpw  37712  bj-imdirco  37812  dissneqlem  37964  relowlssretop  37987  relowlpssretop  37988  ctbssinf  38030  pibt2  38041  matunitlindflem1  38245  ptrecube  38249  poimirlem29  38278  mblfinlem2  38287  mblfinlem3  38288  mblfinlem4  38289  ismblfin  38290  ovoliunnfl  38291  voliunnfl  38293  volsupnfl  38294  indexa  38362  indexdom  38363  neificl  38382  istotbnd3  38400  sstotbnd2  38403  sstotbnd  38404  equivtotbnd  38407  ssbnd  38417  heiborlem1  38440  heiborlem6  38445  heiborlem8  38447  heiborlem10  38449  unichnidl  38660  pridl  38666  ismaxidl  38669  igenval  38690  igenval2  38695  ispridlc  38699  relcnveq3  38954  iss2  38971  brssr  39208  elrelscnveq3  39254  lsmsat  39760  lssatomic  39763  lssats  39764  lsat0cv  39785  lcvexchlem4  39789  lcvexchlem5  39790  lsatcvatlem  39801  l1cvpat  39806  ispsubsp  40497  linepsubN  40504  pclvalN  40642  ispsubclN  40689  ispsubcl2N  40699  pclfinclN  40702  diaelrnN  41797  docavalN  41875  dochval  42103  dvh4dimat  42190  dochexmidlem1  42212  lpolconN  42239  mapdordlem2  42389  eqresfnbd  42981  ismrcd1  43409  ismrcd2  43410  ismrc  43412  mzpcompact2lem  43462  aomclem6  43766  hbtlem6  43836  onintunirab  43934  rp-brsslt  44129  ssficl  44275  ssuncl  44276  ssdifcl  44277  sssymdifcl  44278  elmapintrab  44282  clcnvlem  44329  iunrelexpmin1  44414  iunrelexpmin2  44418  clsk3nimkb  44746  clsk1indlem1  44751  isotone1  44754  isotone2  44755  ntrclsiso  44773  gneispace  44840  gneispacess2  44852  onfrALTlem5  45231  onfrALTlem5VD  45573  relpfrlem  45642  modelaxreplem1  45667  islptre  46315  dvmptconst  46609  dvmptidg  46611  dvmulcncf  46619  dvdivcncf  46621  dvmptfprod  46639  stoweidlem51  46745  stoweidlem52  46746  fourierdlem103  46903  fourierdlem104  46904  ioorrnopnlem  46998  ioorrnopnxrlem  47000  salgenval  47015  ovnval2  47239  ovncvrrp  47258  ovnsubaddlem1  47264  ovnsubadd  47266  ovncvr2  47305  hspmbl  47323  elsetpreimafvssdm  48112  isubgredg  48608  uhgrimisgrgriclem  48672  grimedg  48677  grtrissvtx  48686  grtrimap  48690  stgredgiun  48700  isubgr3stgrlem6  48713  isubgr3stgrlem7  48714  uspgrlimlem1  48730  uspgrlimlem2  48731  uspgrlimlem3  48732  uspgrlimlem4  48733  clnbgrvtxedg  48736  grlimedgclnbgr  48737  grlimpredg  48740  grlimprclnbgrvtx  48741  grlimgredgex  48742  grlimgrtrilem1  48743  grlimgrtrilem2  48744  grlimgrtri  48745  usgrexmpl1lem  48763  usgrexmpl2lem  48768  uspgrsprfo  48890  unilbss  49573  sepfsepc  49683  unilbeu  49740  ipolubdm  49742  ipoglbdm  49745  discsubc  49819  iinfconstbas  49821  setrec1lem1  50442  setrec1lem4  50445  setrec2fun  50447  elsetrecslem  50454  elpglem2  50467