Theorem sseq1 3948

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 3938	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3929	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3929	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	2, 3	anbiim 642	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
5	4	ancoms 458	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
6	1, 5	sylbi 217	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  sseq12  3950  sseq1i  3951  sseq1d  3954  nssne2  3986  psseq1  4031  uneqdifeq  4433  sbss  4461  pwjust  4543  elpwg  4545  pwpw0  4757  sssn  4770  ssunsn2  4771  unimax  4888  trss  5203  al0ssb  5243  sseliALT  5244  elssabg  5280  intabs  5286  vpwex  5314  nnullss  5409  exss  5410  releq  5726  iss  5994  relcnvtrg  6225  fununi  6567  ssimaex  6919  isofrlem  7288  onssmin  7739  tfis  7799  tfisi  7803  funcnvuni  7876  ffoss  7892  f1oweALT  7918  frxp  8069  frxp2  8087  frrlem1  8229  frrlem13  8241  tfrlem1  8308  oawordeu  8483  coflton  8600  cofon1  8601  cofon2  8602  naddunif  8622  qsss  8715  boxcutc  8882  sbthlem2  9019  sbth  9028  findcard2d  9094  ssfi  9100  sbthfi  9126  php  9134  isinf  9168  unbnn2  9200  domunfican  9225  fiint  9230  finsschain  9262  indexfi  9263  dffi3  9337  hartogslem1  9450  cantnfval2  9581  cantnfle  9583  cantnflem1  9601  tz9.1  9641  tcvalg  9648  setind  9659  frmin  9664  scott0  9801  bnd2  9808  carduni  9896  cardaleph  10002  alephinit  10008  aceq3lem  10033  dfac12lem3  10059  infmap2  10130  cflem  10158  cflemOLD  10159  cflm  10163  cflecard  10166  cfeq0  10169  cfsuc  10170  cfflb  10172  cfslb  10179  cfslb2n  10181  coftr  10186  fin23lem13  10245  fin23lem16  10248  fin23lem19  10249  fin23lem29  10254  fin1a2lem13  10325  itunitc  10334  domtriomlem  10355  axdc3lem2  10364  zorn2lem7  10415  zornn0g  10418  pwfseqlem4a  10575  pwfseqlem4  10576  wunfi  10635  wunex2  10652  wuncval  10656  rankcf  10691  tskuni  10697  axgroth6  10742  axgroth3  10745  axgroth4  10746  fzoss1  13632  fsuppmapnn0fiubex  13945  hashf1lem2  14409  cleq1lem  14935  rtrclreclem4  15014  sumeq1  15642  fsumcvg3  15682  fsum2d  15724  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  prodeq1f  15862  prodeq1  15863  fprod2d  15937  lcmfunsnlem  16601  coprmprod  16621  vdwmc  16940  prmgaplem3  17015  prmgaplem4  17016  restsspw  17385  ismred2  17556  mrcval  17567  mrcuni  17578  acsfn  17616  isssc  17778  drsdirfi  18262  ipodrsima  18498  cntzssv  19294  pmtrfrn  19424  pmtrrn2  19426  pmtrdifellem1  19442  pmtrdifellem2  19443  sylow2alem2  19584  sylow2a  19585  efgval  19683  gsumzaddlem  19887  ablfac1eulem  20040  gsumle  20111  rgspnval  20580  lspval  20961  lspindpi  21122  znf1o  21541  zntoslem  21546  aspval  21862  mplsubglem  21987  mpllsslem  21988  mplcoe1  22025  mplcoe5  22028  mdetunilem9  22595  uniopn  22872  fiinopn  22876  fiinbas  22927  baspartn  22929  eltg2  22933  eltg3  22937  topbas  22947  pptbas  22983  clsval  23012  neiint  23079  neips  23088  opnneissb  23089  opnssneib  23090  innei  23100  neiptoptop  23106  neiptopnei  23107  restbas  23133  restcld  23147  neitr  23155  restcls  23156  restntr  23157  cnpdis  23268  cmpsublem  23374  cmpsub  23375  fiuncmp  23379  unconn  23404  1stcfb  23420  2ndc1stc  23426  1stcrest  23428  2ndcctbss  23430  2ndcomap  23433  dis2ndc  23435  lly1stc  23471  refssex  23486  refun0  23490  llycmpkgen2  23525  txbas  23542  eltx  23543  ptuni2  23551  neitx  23582  ptpjopn  23587  ptcld  23588  txlm  23623  tx1stc  23625  txkgen  23627  xkopt  23630  xkococnlem  23634  ptcmpfi  23788  fbssfi  23812  opnfbas  23817  isfil2  23831  isfildlem  23832  snfil  23839  fsubbas  23842  ssfg  23847  fgss2  23849  fgcl  23853  fbasrn  23859  fgtr  23865  ufli  23889  uffix  23896  rnelfmlem  23927  fclscf  24000  alexsublem  24019  alexsubALTlem2  24023  alexsubALTlem3  24024  alexsubALTlem4  24025  alexsubALT  24026  tmdgsum2  24071  subgntr  24082  opnsubg  24083  qustgpopn  24095  tsmsfbas  24103  tsmsgsum  24114  tsmsres  24119  tsmsf1o  24120  tsmsxplem1  24128  tsmsxp  24130  isust  24179  ustssel  24181  ustincl  24183  ustdiag  24184  ustinvel  24185  ustexhalf  24186  ustexsym  24191  ust0  24195  restutop  24212  ustuqtop4  24219  utopsnneiplem  24222  blssexps  24401  blssex  24402  neibl  24476  blcld  24480  met1stc  24496  met2ndci  24497  metrest  24499  prdsxmslem2  24504  metustfbas  24532  cfilucfil  24534  metuel2  24540  metustbl  24541  restmetu  24545  dscopn  24548  isngp2  24572  tgioo  24771  tgqioo  24775  zdis  24792  xrge0tsms  24810  fsumcn  24847  volivth  25584  vitalilem2  25586  itgfsum  25804  limcun  25872  recnprss  25881  dvmptfsum  25952  ftc1a  26014  plyssc  26175  efopn  26635  jensen  26966  brslts  27768  madef  27842  tglnunirn  28630  lpvtx  29151  umgredgprv  29190  usgredgprvALT  29278  issubgr2  29355  subgrprop2  29357  egrsubgr  29360  0uhgrsubgr  29362  frcond3  30354  hhsssh  31355  shintcl  31416  chintcl  31418  spanval  31419  omlsi  31490  pjoml  31522  chnlen0  31530  chsscon3  31586  chlejb1  31598  chnle  31600  spanun  31631  h1datom  31668  cmbr4i  31687  pjoml2  31697  pjoml3  31698  lecm  31703  osumcor2i  31730  osum  31731  spansncv  31739  pjcjt2  31778  pjopyth  31806  hstel2  32305  stj  32321  stcltr1i  32360  mdi  32381  mdbr3  32383  mdbr4  32384  dmdbr  32385  dmdmd  32386  dmdbr5  32394  mdsl1i  32407  mdslmd1lem3  32413  mdslmd1lem4  32414  mdslmd1i  32415  csmdsymi  32420  atss  32432  atom1d  32439  superpos  32440  chcv1  32441  shatomici  32444  shatomistici  32447  hatomistici  32448  chrelat2  32456  chirredi  32480  atcvat4i  32483  mdsymlem2  32490  mdsymlem6  32494  dmdbr6ati  32509  dmdbr7ati  32510  xrge0tsmsd  33149  gsumvsca1  33302  gsumvsca2  33303  prmidl  33515  ismxidl  33537  constrfiss  33911  zarcls1  34029  zarclsun  34030  zarclsiin  34031  zarclsint  34032  zarclssn  34033  zartop  34036  zartopon  34037  zart0  34039  zarmxt1  34040  zarcmp  34042  rhmpreimacnlem  34044  rhmpreimacn  34045  tpr2rico  34072  issiga  34272  isrnsiga  34273  sigagenval  34300  measiuns  34377  dya2icoseg  34437  dya2iocnrect  34441  dya2iocuni  34443  carsgmon  34474  carsgsigalem  34475  carsgclctunlem2  34479  carsgclctun  34481  pmeasmono  34484  pmeasadd  34485  bnj517  35043  bnj1118  35142  bnj1145  35151  bnj1154  35157  bnj1452  35210  bnj1498  35219  fineqvpow  35275  fineqvac  35276  fineqvacALT  35277  setindregs  35290  tz9.1regs  35294  fineqvr1ombregs  35298  vonf1owev  35306  pthhashvtx  35326  kur14lem1  35404  cvmopnlem  35476  dfon2lem3  35981  dfon2lem7  35985  brsset  36085  fness  36547  fneref  36548  fnessref  36555  neibastop2lem  36558  topmeet  36562  fnejoin2  36567  tailfb  36575  filnetlem4  36579  onsucsuccmpi  36641  ttcwf2  36723  ttcexg  36730  bj-snglss  37293  bj-elpwgALT  37377  bj-restpw  37420  bj-imdirco  37520  dissneqlem  37670  relowlssretop  37693  relowlpssretop  37694  ctbssinf  37736  pibt2  37747  matunitlindflem1  37951  ptrecube  37955  poimirlem29  37984  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  indexa  38068  indexdom  38069  neificl  38088  istotbnd3  38106  sstotbnd2  38109  sstotbnd  38110  equivtotbnd  38113  ssbnd  38123  heiborlem1  38146  heiborlem6  38151  heiborlem8  38153  heiborlem10  38155  unichnidl  38366  pridl  38372  ismaxidl  38375  igenval  38396  igenval2  38401  ispridlc  38405  relcnveq3  38662  iss2  38679  brssr  38916  elrelscnveq3  38962  lsmsat  39468  lssatomic  39471  lssats  39472  lsat0cv  39493  lcvexchlem4  39497  lcvexchlem5  39498  lsatcvatlem  39509  l1cvpat  39514  ispsubsp  40205  linepsubN  40212  pclvalN  40350  ispsubclN  40397  ispsubcl2N  40407  pclfinclN  40410  diaelrnN  41505  docavalN  41583  dochval  41811  dvh4dimat  41898  dochexmidlem1  41920  lpolconN  41947  mapdordlem2  42097  eqresfnbd  42687  ismrcd1  43144  ismrcd2  43145  ismrc  43147  mzpcompact2lem  43197  aomclem6  43505  hbtlem6  43575  onintunirab  43673  rp-brsslt  43868  ssficl  44014  ssuncl  44015  ssdifcl  44016  sssymdifcl  44017  elmapintrab  44021  clcnvlem  44068  iunrelexpmin1  44153  iunrelexpmin2  44157  clsk3nimkb  44485  clsk1indlem1  44490  isotone1  44493  isotone2  44494  ntrclsiso  44512  gneispace  44579  gneispacess2  44591  onfrALTlem5  44987  onfrALTlem5VD  45329  relpfrlem  45398  modelaxreplem1  45423  islptre  46067  dvmptconst  46361  dvmptidg  46363  dvmulcncf  46371  dvdivcncf  46373  dvmptfprod  46391  stoweidlem51  46497  stoweidlem52  46498  fourierdlem103  46655  fourierdlem104  46656  ioorrnopnlem  46750  ioorrnopnxrlem  46752  salgenval  46767  ovnval2  46991  ovncvrrp  47010  ovnsubaddlem1  47016  ovnsubadd  47018  ovncvr2  47057  hspmbl  47075  elsetpreimafvssdm  47858  isubgredg  48354  uhgrimisgrgriclem  48418  grimedg  48423  grtrissvtx  48432  grtrimap  48436  stgredgiun  48446  isubgr3stgrlem6  48459  isubgr3stgrlem7  48460  uspgrlimlem1  48476  uspgrlimlem2  48477  uspgrlimlem3  48478  uspgrlimlem4  48479  clnbgrvtxedg  48482  grlimedgclnbgr  48483  grlimpredg  48486  grlimprclnbgrvtx  48487  grlimgredgex  48488  grlimgrtrilem1  48489  grlimgrtrilem2  48490  grlimgrtri  48491  usgrexmpl1lem  48509  usgrexmpl2lem  48514  uspgrsprfo  48636  unilbss  49305  sepfsepc  49415  unilbeu  49472  ipolubdm  49474  ipoglbdm  49477  discsubc  49551  iinfconstbas  49553  setrec1lem1  50174  setrec1lem4  50177  setrec2fun  50179  elsetrecslem  50186  elpglem2  50199