Theorem sseq1 3960

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919

This theorem is referenced by:  sseq12  3962  sseq1i  3963  sseq1d  3966  nssne2  3998  psseq1  4040  uneqdifeq  4443  sbss  4469  pwjust  4551  elpwg  4553  pwpw0  4765  sssn  4778  ssunsn2  4779  unimax  4895  trss  5208  al0ssb  5246  sseliALT  5247  elssabg  5281  intabs  5287  vpwex  5315  nnullss  5402  exss  5403  releq  5717  iss  5984  relcnvtrg  6214  fununi  6556  ssimaex  6907  isofrlem  7274  onssmin  7725  tfis  7785  tfisi  7789  funcnvuni  7862  ffoss  7878  f1oweALT  7904  frxp  8056  frxp2  8074  frrlem1  8216  frrlem13  8228  tfrlem1  8295  oawordeu  8470  coflton  8586  cofon1  8587  cofon2  8588  naddunif  8608  qsss  8700  boxcutc  8865  sbthlem2  9001  sbth  9010  findcard2d  9076  ssfi  9082  sbthfi  9108  php  9116  isinf  9149  unbnn2  9181  domunfican  9206  fiint  9211  finsschain  9243  indexfi  9244  dffi3  9315  hartogslem1  9428  cantnfval2  9559  cantnfle  9561  cantnflem1  9579  tz9.1  9619  setind  9624  tcvalg  9628  frmin  9639  scott0  9776  bnd2  9783  carduni  9871  cardaleph  9977  alephinit  9983  aceq3lem  10008  dfac12lem3  10034  infmap2  10105  cflem  10133  cflemOLD  10134  cflm  10138  cflecard  10141  cfeq0  10144  cfsuc  10145  cfflb  10147  cfslb  10154  cfslb2n  10156  coftr  10161  fin23lem13  10220  fin23lem16  10223  fin23lem19  10224  fin23lem29  10229  fin1a2lem13  10300  itunitc  10309  domtriomlem  10330  axdc3lem2  10339  zorn2lem7  10390  zornn0g  10393  pwfseqlem4a  10549  pwfseqlem4  10550  wunfi  10609  wunex2  10626  wuncval  10630  rankcf  10665  tskuni  10671  axgroth6  10716  axgroth3  10719  axgroth4  10720  fzoss1  13583  fsuppmapnn0fiubex  13896  hashf1lem2  14360  cleq1lem  14886  rtrclreclem4  14965  sumeq1  15593  fsumcvg3  15633  fsum2d  15675  fsumabs  15705  fsumrlim  15715  fsumo1  15716  fsumiun  15725  prodeq1f  15810  prodeq1  15811  fprod2d  15885  lcmfunsnlem  16549  coprmprod  16569  vdwmc  16887  prmgaplem3  16962  prmgaplem4  16963  restsspw  17332  ismred2  17502  mrcval  17513  mrcuni  17524  acsfn  17562  isssc  17724  drsdirfi  18208  ipodrsima  18444  cntzssv  19238  pmtrfrn  19368  pmtrrn2  19370  pmtrdifellem1  19386  pmtrdifellem2  19387  sylow2alem2  19528  sylow2a  19529  efgval  19627  gsumzaddlem  19831  ablfac1eulem  19984  gsumle  20055  rgspnval  20525  lspval  20906  lspindpi  21067  znf1o  21486  zntoslem  21491  aspval  21808  mplsubglem  21934  mpllsslem  21935  mplcoe1  21970  mplcoe5  21973  mdetunilem9  22533  uniopn  22810  fiinopn  22814  fiinbas  22865  baspartn  22867  eltg2  22871  eltg3  22875  topbas  22885  pptbas  22921  clsval  22950  neiint  23017  neips  23026  opnneissb  23027  opnssneib  23028  innei  23038  neiptoptop  23044  neiptopnei  23045  restbas  23071  restcld  23085  neitr  23093  restcls  23094  restntr  23095  cnpdis  23206  cmpsublem  23312  cmpsub  23313  fiuncmp  23317  unconn  23342  1stcfb  23358  2ndc1stc  23364  1stcrest  23366  2ndcctbss  23368  2ndcomap  23371  dis2ndc  23373  lly1stc  23409  refssex  23424  refun0  23428  llycmpkgen2  23463  txbas  23480  eltx  23481  ptuni2  23489  neitx  23520  ptpjopn  23525  ptcld  23526  txlm  23561  tx1stc  23563  txkgen  23565  xkopt  23568  xkococnlem  23572  ptcmpfi  23726  fbssfi  23750  opnfbas  23755  isfil2  23769  isfildlem  23770  snfil  23777  fsubbas  23780  ssfg  23785  fgss2  23787  fgcl  23791  fbasrn  23797  fgtr  23803  ufli  23827  uffix  23834  rnelfmlem  23865  fclscf  23938  alexsublem  23957  alexsubALTlem2  23961  alexsubALTlem3  23962  alexsubALTlem4  23963  alexsubALT  23964  tmdgsum2  24009  subgntr  24020  opnsubg  24021  qustgpopn  24033  tsmsfbas  24041  tsmsgsum  24052  tsmsres  24057  tsmsf1o  24058  tsmsxplem1  24066  tsmsxp  24068  isust  24117  ustssel  24119  ustincl  24121  ustdiag  24122  ustinvel  24123  ustexhalf  24124  ustexsym  24129  ust0  24133  restutop  24150  ustuqtop4  24157  utopsnneiplem  24160  blssexps  24339  blssex  24340  neibl  24414  blcld  24418  met1stc  24434  met2ndci  24435  metrest  24437  prdsxmslem2  24442  metustfbas  24470  cfilucfil  24472  metuel2  24478  metustbl  24479  restmetu  24483  dscopn  24486  isngp2  24510  tgioo  24709  tgqioo  24713  zdis  24730  xrge0tsms  24748  fsumcn  24786  volivth  25533  vitalilem2  25535  itgfsum  25753  limcun  25821  recnprss  25830  dvmptfsum  25904  ftc1a  25969  plyssc  26130  efopn  26592  jensen  26924  brsslt  27723  madef  27795  tglnunirn  28524  lpvtx  29044  umgredgprv  29083  usgredgprvALT  29171  issubgr2  29248  subgrprop2  29250  egrsubgr  29253  0uhgrsubgr  29255  frcond3  30244  hhsssh  31244  shintcl  31305  chintcl  31307  spanval  31308  omlsi  31379  pjoml  31411  chnlen0  31419  chsscon3  31475  chlejb1  31487  chnle  31489  spanun  31520  h1datom  31557  cmbr4i  31576  pjoml2  31586  pjoml3  31587  lecm  31592  osumcor2i  31619  osum  31620  spansncv  31628  pjcjt2  31667  pjopyth  31695  hstel2  32194  stj  32210  stcltr1i  32249  mdi  32270  mdbr3  32272  mdbr4  32273  dmdbr  32274  dmdmd  32275  dmdbr5  32283  mdsl1i  32296  mdslmd1lem3  32302  mdslmd1lem4  32303  mdslmd1i  32304  csmdsymi  32309  atss  32321  atom1d  32328  superpos  32329  chcv1  32330  shatomici  32333  shatomistici  32336  hatomistici  32337  chrelat2  32345  chirredi  32369  atcvat4i  32372  mdsymlem2  32379  mdsymlem6  32383  dmdbr6ati  32398  dmdbr7ati  32399  xrge0tsmsd  33037  gsumvsca1  33190  gsumvsca2  33191  prmidl  33400  ismxidl  33422  constrfiss  33759  zarcls1  33877  zarclsun  33878  zarclsiin  33879  zarclsint  33880  zarclssn  33881  zartop  33884  zartopon  33885  zart0  33887  zarmxt1  33888  zarcmp  33890  rhmpreimacnlem  33892  rhmpreimacn  33893  tpr2rico  33920  issiga  34120  isrnsiga  34121  sigagenval  34148  measiuns  34225  dya2icoseg  34285  dya2iocnrect  34289  dya2iocuni  34291  carsgmon  34322  carsgsigalem  34323  carsgclctunlem2  34327  carsgclctun  34329  pmeasmono  34332  pmeasadd  34333  bnj517  34892  bnj1118  34991  bnj1145  35000  bnj1154  35006  bnj1452  35059  bnj1498  35068  setindregs  35116  tz9.1regs  35118  fineqvr1ombregs  35123  fineqvpow  35126  fineqvac  35127  fineqvacALT  35128  vonf1owev  35140  pthhashvtx  35160  kur14lem1  35238  cvmopnlem  35310  dfon2lem3  35818  dfon2lem7  35822  brsset  35922  fness  36382  fneref  36383  fnessref  36390  neibastop2lem  36393  topmeet  36397  fnejoin2  36402  tailfb  36410  filnetlem4  36414  onsucsuccmpi  36476  bj-snglss  37003  bj-elpwgALT  37087  bj-restpw  37125  bj-imdirco  37223  dissneqlem  37373  relowlssretop  37396  relowlpssretop  37397  ctbssinf  37439  pibt2  37450  matunitlindflem1  37655  ptrecube  37659  poimirlem29  37688  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  indexa  37772  indexdom  37773  neificl  37792  istotbnd3  37810  sstotbnd2  37813  sstotbnd  37814  equivtotbnd  37817  ssbnd  37827  heiborlem1  37850  heiborlem6  37855  heiborlem8  37857  heiborlem10  37859  unichnidl  38070  pridl  38076  ismaxidl  38079  igenval  38100  igenval2  38105  ispridlc  38109  relcnveq3  38354  iss2  38371  elrelscnveq3  38527  brssr  38537  lsmsat  39046  lssatomic  39049  lssats  39050  lsat0cv  39071  lcvexchlem4  39075  lcvexchlem5  39076  lsatcvatlem  39087  l1cvpat  39092  ispsubsp  39783  linepsubN  39790  pclvalN  39928  ispsubclN  39975  ispsubcl2N  39985  pclfinclN  39988  diaelrnN  41083  docavalN  41161  dochval  41389  dvh4dimat  41476  dochexmidlem1  41498  lpolconN  41525  mapdordlem2  41675  eqresfnbd  42264  ismrcd1  42730  ismrcd2  42731  ismrc  42733  mzpcompact2lem  42783  aomclem6  43091  hbtlem6  43161  onintunirab  43259  rp-brsslt  43455  ssficl  43601  ssuncl  43602  ssdifcl  43603  sssymdifcl  43604  elmapintrab  43608  clcnvlem  43655  iunrelexpmin1  43740  iunrelexpmin2  43744  clsk3nimkb  44072  clsk1indlem1  44077  isotone1  44080  isotone2  44081  ntrclsiso  44099  gneispace  44166  gneispacess2  44178  onfrALTlem5  44574  onfrALTlem5VD  44916  relpfrlem  44985  modelaxreplem1  45010  islptre  45658  dvmptconst  45952  dvmptidg  45954  dvmulcncf  45962  dvdivcncf  45964  dvmptfprod  45982  stoweidlem51  46088  stoweidlem52  46089  fourierdlem103  46246  fourierdlem104  46247  ioorrnopnlem  46341  ioorrnopnxrlem  46343  salgenval  46358  ovnval2  46582  ovncvrrp  46601  ovnsubaddlem1  46607  ovnsubadd  46609  ovncvr2  46648  hspmbl  46666  elsetpreimafvssdm  47416  isubgredg  47896  uhgrimisgrgriclem  47960  grimedg  47965  grtrissvtx  47974  grtrimap  47978  stgredgiun  47988  isubgr3stgrlem6  48001  isubgr3stgrlem7  48002  uspgrlimlem1  48018  uspgrlimlem2  48019  uspgrlimlem3  48020  uspgrlimlem4  48021  clnbgrvtxedg  48024  grlimedgclnbgr  48025  grlimpredg  48028  grlimprclnbgrvtx  48029  grlimgredgex  48030  grlimgrtrilem1  48031  grlimgrtrilem2  48032  grlimgrtri  48033  usgrexmpl1lem  48051  usgrexmpl2lem  48056  uspgrsprfo  48178  unilbss  48848  sepfsepc  48958  unilbeu  49015  ipolubdm  49017  ipoglbdm  49020  discsubc  49095  iinfconstbas  49097  setrec1lem1  49718  setrec1lem4  49721  setrec2fun  49723  elsetrecslem  49730  elpglem2  49743