Theorem sseq1 3959

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 3949	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3940	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3940	. . . 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 3901

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 2123  ax-ext 2708

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

This theorem is referenced by:  sseq12  3961  sseq1i  3962  sseq1d  3965  nssne2  3997  psseq1  4042  uneqdifeq  4445  sbss  4473  pwjust  4555  elpwg  4557  pwpw0  4769  sssn  4782  ssunsn2  4783  unimax  4900  trss  5215  al0ssb  5253  sseliALT  5254  elssabg  5288  intabs  5294  vpwex  5322  nnullss  5410  exss  5411  releq  5726  iss  5994  relcnvtrg  6225  fununi  6567  ssimaex  6919  isofrlem  7286  onssmin  7737  tfis  7797  tfisi  7801  funcnvuni  7874  ffoss  7890  f1oweALT  7916  frxp  8068  frxp2  8086  frrlem1  8228  frrlem13  8240  tfrlem1  8307  oawordeu  8482  coflton  8599  cofon1  8600  cofon2  8601  naddunif  8621  qsss  8713  boxcutc  8879  sbthlem2  9016  sbth  9025  findcard2d  9091  ssfi  9097  sbthfi  9123  php  9131  isinf  9165  unbnn2  9197  domunfican  9222  fiint  9227  finsschain  9259  indexfi  9260  dffi3  9334  hartogslem1  9447  cantnfval2  9578  cantnfle  9580  cantnflem1  9598  tz9.1  9638  tcvalg  9645  setind  9656  frmin  9661  scott0  9798  bnd2  9805  carduni  9893  cardaleph  9999  alephinit  10005  aceq3lem  10030  dfac12lem3  10056  infmap2  10127  cflem  10155  cflemOLD  10156  cflm  10160  cflecard  10163  cfeq0  10166  cfsuc  10167  cfflb  10169  cfslb  10176  cfslb2n  10178  coftr  10183  fin23lem13  10242  fin23lem16  10245  fin23lem19  10246  fin23lem29  10251  fin1a2lem13  10322  itunitc  10331  domtriomlem  10352  axdc3lem2  10361  zorn2lem7  10412  zornn0g  10415  pwfseqlem4a  10572  pwfseqlem4  10573  wunfi  10632  wunex2  10649  wuncval  10653  rankcf  10688  tskuni  10694  axgroth6  10739  axgroth3  10742  axgroth4  10743  fzoss1  13602  fsuppmapnn0fiubex  13915  hashf1lem2  14379  cleq1lem  14905  rtrclreclem4  14984  sumeq1  15612  fsumcvg3  15652  fsum2d  15694  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  prodeq1f  15829  prodeq1  15830  fprod2d  15904  lcmfunsnlem  16568  coprmprod  16588  vdwmc  16906  prmgaplem3  16981  prmgaplem4  16982  restsspw  17351  ismred2  17522  mrcval  17533  mrcuni  17544  acsfn  17582  isssc  17744  drsdirfi  18228  ipodrsima  18464  cntzssv  19257  pmtrfrn  19387  pmtrrn2  19389  pmtrdifellem1  19405  pmtrdifellem2  19406  sylow2alem2  19547  sylow2a  19548  efgval  19646  gsumzaddlem  19850  ablfac1eulem  20003  gsumle  20074  rgspnval  20545  lspval  20926  lspindpi  21087  znf1o  21506  zntoslem  21511  aspval  21828  mplsubglem  21954  mpllsslem  21955  mplcoe1  21992  mplcoe5  21995  mdetunilem9  22564  uniopn  22841  fiinopn  22845  fiinbas  22896  baspartn  22898  eltg2  22902  eltg3  22906  topbas  22916  pptbas  22952  clsval  22981  neiint  23048  neips  23057  opnneissb  23058  opnssneib  23059  innei  23069  neiptoptop  23075  neiptopnei  23076  restbas  23102  restcld  23116  neitr  23124  restcls  23125  restntr  23126  cnpdis  23237  cmpsublem  23343  cmpsub  23344  fiuncmp  23348  unconn  23373  1stcfb  23389  2ndc1stc  23395  1stcrest  23397  2ndcctbss  23399  2ndcomap  23402  dis2ndc  23404  lly1stc  23440  refssex  23455  refun0  23459  llycmpkgen2  23494  txbas  23511  eltx  23512  ptuni2  23520  neitx  23551  ptpjopn  23556  ptcld  23557  txlm  23592  tx1stc  23594  txkgen  23596  xkopt  23599  xkococnlem  23603  ptcmpfi  23757  fbssfi  23781  opnfbas  23786  isfil2  23800  isfildlem  23801  snfil  23808  fsubbas  23811  ssfg  23816  fgss2  23818  fgcl  23822  fbasrn  23828  fgtr  23834  ufli  23858  uffix  23865  rnelfmlem  23896  fclscf  23969  alexsublem  23988  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  alexsubALT  23995  tmdgsum2  24040  subgntr  24051  opnsubg  24052  qustgpopn  24064  tsmsfbas  24072  tsmsgsum  24083  tsmsres  24088  tsmsf1o  24089  tsmsxplem1  24097  tsmsxp  24099  isust  24148  ustssel  24150  ustincl  24152  ustdiag  24153  ustinvel  24154  ustexhalf  24155  ustexsym  24160  ust0  24164  restutop  24181  ustuqtop4  24188  utopsnneiplem  24191  blssexps  24370  blssex  24371  neibl  24445  blcld  24449  met1stc  24465  met2ndci  24466  metrest  24468  prdsxmslem2  24473  metustfbas  24501  cfilucfil  24503  metuel2  24509  metustbl  24510  restmetu  24514  dscopn  24517  isngp2  24541  tgioo  24740  tgqioo  24744  zdis  24761  xrge0tsms  24779  fsumcn  24817  volivth  25564  vitalilem2  25566  itgfsum  25784  limcun  25852  recnprss  25861  dvmptfsum  25935  ftc1a  26000  plyssc  26161  efopn  26623  jensen  26955  brslts  27758  madef  27832  tglnunirn  28620  lpvtx  29141  umgredgprv  29180  usgredgprvALT  29268  issubgr2  29345  subgrprop2  29347  egrsubgr  29350  0uhgrsubgr  29352  frcond3  30344  hhsssh  31344  shintcl  31405  chintcl  31407  spanval  31408  omlsi  31479  pjoml  31511  chnlen0  31519  chsscon3  31575  chlejb1  31587  chnle  31589  spanun  31620  h1datom  31657  cmbr4i  31676  pjoml2  31686  pjoml3  31687  lecm  31692  osumcor2i  31719  osum  31720  spansncv  31728  pjcjt2  31767  pjopyth  31795  hstel2  32294  stj  32310  stcltr1i  32349  mdi  32370  mdbr3  32372  mdbr4  32373  dmdbr  32374  dmdmd  32375  dmdbr5  32383  mdsl1i  32396  mdslmd1lem3  32402  mdslmd1lem4  32403  mdslmd1i  32404  csmdsymi  32409  atss  32421  atom1d  32428  superpos  32429  chcv1  32430  shatomici  32433  shatomistici  32436  hatomistici  32437  chrelat2  32445  chirredi  32469  atcvat4i  32472  mdsymlem2  32479  mdsymlem6  32483  dmdbr6ati  32498  dmdbr7ati  32499  xrge0tsmsd  33155  gsumvsca1  33308  gsumvsca2  33309  prmidl  33521  ismxidl  33543  constrfiss  33908  zarcls1  34026  zarclsun  34027  zarclsiin  34028  zarclsint  34029  zarclssn  34030  zartop  34033  zartopon  34034  zart0  34036  zarmxt1  34037  zarcmp  34039  rhmpreimacnlem  34041  rhmpreimacn  34042  tpr2rico  34069  issiga  34269  isrnsiga  34270  sigagenval  34297  measiuns  34374  dya2icoseg  34434  dya2iocnrect  34438  dya2iocuni  34440  carsgmon  34471  carsgsigalem  34472  carsgclctunlem2  34476  carsgclctun  34478  pmeasmono  34481  pmeasadd  34482  bnj517  35041  bnj1118  35140  bnj1145  35149  bnj1154  35155  bnj1452  35208  bnj1498  35217  fineqvpow  35271  fineqvac  35272  fineqvacALT  35273  setindregs  35286  tz9.1regs  35290  fineqvr1ombregs  35294  vonf1owev  35302  pthhashvtx  35322  kur14lem1  35400  cvmopnlem  35472  dfon2lem3  35977  dfon2lem7  35981  brsset  36081  fness  36543  fneref  36544  fnessref  36551  neibastop2lem  36554  topmeet  36558  fnejoin2  36563  tailfb  36571  filnetlem4  36575  onsucsuccmpi  36637  bj-snglss  37171  bj-elpwgALT  37255  bj-restpw  37293  bj-imdirco  37391  dissneqlem  37541  relowlssretop  37564  relowlpssretop  37565  ctbssinf  37607  pibt2  37618  matunitlindflem1  37813  ptrecube  37817  poimirlem29  37846  mblfinlem2  37855  mblfinlem3  37856  mblfinlem4  37857  ismblfin  37858  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  indexa  37930  indexdom  37931  neificl  37950  istotbnd3  37968  sstotbnd2  37971  sstotbnd  37972  equivtotbnd  37975  ssbnd  37985  heiborlem1  38008  heiborlem6  38013  heiborlem8  38015  heiborlem10  38017  unichnidl  38228  pridl  38234  ismaxidl  38237  igenval  38258  igenval2  38263  ispridlc  38267  relcnveq3  38516  iss2  38533  brssr  38750  elrelscnveq3  38796  lsmsat  39264  lssatomic  39267  lssats  39268  lsat0cv  39289  lcvexchlem4  39293  lcvexchlem5  39294  lsatcvatlem  39305  l1cvpat  39310  ispsubsp  40001  linepsubN  40008  pclvalN  40146  ispsubclN  40193  ispsubcl2N  40203  pclfinclN  40206  diaelrnN  41301  docavalN  41379  dochval  41607  dvh4dimat  41694  dochexmidlem1  41716  lpolconN  41743  mapdordlem2  41893  eqresfnbd  42484  ismrcd1  42936  ismrcd2  42937  ismrc  42939  mzpcompact2lem  42989  aomclem6  43297  hbtlem6  43367  onintunirab  43465  rp-brsslt  43660  ssficl  43806  ssuncl  43807  ssdifcl  43808  sssymdifcl  43809  elmapintrab  43813  clcnvlem  43860  iunrelexpmin1  43945  iunrelexpmin2  43949  clsk3nimkb  44277  clsk1indlem1  44282  isotone1  44285  isotone2  44286  ntrclsiso  44304  gneispace  44371  gneispacess2  44383  onfrALTlem5  44779  onfrALTlem5VD  45121  relpfrlem  45190  modelaxreplem1  45215  islptre  45861  dvmptconst  46155  dvmptidg  46157  dvmulcncf  46165  dvdivcncf  46167  dvmptfprod  46185  stoweidlem51  46291  stoweidlem52  46292  fourierdlem103  46449  fourierdlem104  46450  ioorrnopnlem  46544  ioorrnopnxrlem  46546  salgenval  46561  ovnval2  46785  ovncvrrp  46804  ovnsubaddlem1  46810  ovnsubadd  46812  ovncvr2  46851  hspmbl  46869  elsetpreimafvssdm  47628  isubgredg  48108  uhgrimisgrgriclem  48172  grimedg  48177  grtrissvtx  48186  grtrimap  48190  stgredgiun  48200  isubgr3stgrlem6  48213  isubgr3stgrlem7  48214  uspgrlimlem1  48230  uspgrlimlem2  48231  uspgrlimlem3  48232  uspgrlimlem4  48233  clnbgrvtxedg  48236  grlimedgclnbgr  48237  grlimpredg  48240  grlimprclnbgrvtx  48241  grlimgredgex  48242  grlimgrtrilem1  48243  grlimgrtrilem2  48244  grlimgrtri  48245  usgrexmpl1lem  48263  usgrexmpl2lem  48268  uspgrsprfo  48390  unilbss  49059  sepfsepc  49169  unilbeu  49226  ipolubdm  49228  ipoglbdm  49231  discsubc  49305  iinfconstbas  49307  setrec1lem1  49928  setrec1lem4  49931  setrec2fun  49933  elsetrecslem  49940  elpglem2  49953