Theorem sseq1 3975

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 3965	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3956	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3956	. . . 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 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  sseq12  3977  sseq1i  3978  sseq1d  3981  nssne2  4013  psseq1  4056  uneqdifeq  4459  sbss  4485  pwjust  4567  elpwg  4569  pwpw0  4780  sssn  4793  ssunsn2  4794  unimax  4911  trss  5228  al0ssb  5266  sseliALT  5267  elssabg  5301  intabs  5307  vpwex  5335  nnullss  5425  exss  5426  releq  5742  iss  6009  relcnvtrg  6242  fununi  6594  ssimaex  6949  isofrlem  7318  onssmin  7771  tfis  7834  tfisi  7838  funcnvuni  7911  ffoss  7927  f1oweALT  7954  frxp  8108  frxp2  8126  frrlem1  8268  frrlem13  8280  tfrlem1  8347  oawordeu  8522  coflton  8638  cofon1  8639  cofon2  8640  naddunif  8660  qsss  8752  boxcutc  8917  sbthlem2  9058  sbth  9067  findcard2d  9136  ssfi  9143  sbthfi  9169  php  9177  isinf  9214  isinfOLD  9215  unbnn2  9251  domunfican  9279  fiint  9284  fiintOLD  9285  finsschain  9317  indexfi  9318  dffi3  9389  hartogslem1  9502  cantnfval2  9629  cantnfle  9631  cantnflem1  9649  tz9.1  9689  setind  9694  tcvalg  9698  frmin  9709  scott0  9846  bnd2  9853  carduni  9941  cardaleph  10049  alephinit  10055  aceq3lem  10080  dfac12lem3  10106  infmap2  10177  cflem  10205  cflemOLD  10206  cflm  10210  cflecard  10213  cfeq0  10216  cfsuc  10217  cfflb  10219  cfslb  10226  cfslb2n  10228  coftr  10233  fin23lem13  10292  fin23lem16  10295  fin23lem19  10296  fin23lem29  10301  fin1a2lem13  10372  itunitc  10381  domtriomlem  10402  axdc3lem2  10411  zorn2lem7  10462  zornn0g  10465  pwfseqlem4a  10621  pwfseqlem4  10622  wunfi  10681  wunex2  10698  wuncval  10702  rankcf  10737  tskuni  10743  axgroth6  10788  axgroth3  10791  axgroth4  10792  fzoss1  13654  fsuppmapnn0fiubex  13964  hashf1lem2  14428  cleq1lem  14955  rtrclreclem4  15034  sumeq1  15662  fsumcvg3  15702  fsum2d  15744  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fsumiun  15794  prodeq1f  15879  prodeq1  15880  fprod2d  15954  lcmfunsnlem  16618  coprmprod  16638  vdwmc  16956  prmgaplem3  17031  prmgaplem4  17032  restsspw  17401  ismred2  17571  mrcval  17578  mrcuni  17589  acsfn  17627  isssc  17789  drsdirfi  18273  ipodrsima  18507  cntzssv  19267  pmtrfrn  19395  pmtrrn2  19397  pmtrdifellem1  19413  pmtrdifellem2  19414  sylow2alem2  19555  sylow2a  19556  efgval  19654  gsumzaddlem  19858  ablfac1eulem  20011  rgspnval  20528  lspval  20888  lspindpi  21049  znf1o  21468  zntoslem  21473  aspval  21789  mplsubglem  21915  mpllsslem  21916  mplcoe1  21951  mplcoe5  21954  mdetunilem9  22514  uniopn  22791  fiinopn  22795  fiinbas  22846  baspartn  22848  eltg2  22852  eltg3  22856  topbas  22866  pptbas  22902  clsval  22931  neiint  22998  neips  23007  opnneissb  23008  opnssneib  23009  innei  23019  neiptoptop  23025  neiptopnei  23026  restbas  23052  restcld  23066  neitr  23074  restcls  23075  restntr  23076  cnpdis  23187  cmpsublem  23293  cmpsub  23294  fiuncmp  23298  unconn  23323  1stcfb  23339  2ndc1stc  23345  1stcrest  23347  2ndcctbss  23349  2ndcomap  23352  dis2ndc  23354  lly1stc  23390  refssex  23405  refun0  23409  llycmpkgen2  23444  txbas  23461  eltx  23462  ptuni2  23470  neitx  23501  ptpjopn  23506  ptcld  23507  txlm  23542  tx1stc  23544  txkgen  23546  xkopt  23549  xkococnlem  23553  ptcmpfi  23707  fbssfi  23731  opnfbas  23736  isfil2  23750  isfildlem  23751  snfil  23758  fsubbas  23761  ssfg  23766  fgss2  23768  fgcl  23772  fbasrn  23778  fgtr  23784  ufli  23808  uffix  23815  rnelfmlem  23846  fclscf  23919  alexsublem  23938  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  alexsubALT  23945  tmdgsum2  23990  subgntr  24001  opnsubg  24002  qustgpopn  24014  tsmsfbas  24022  tsmsgsum  24033  tsmsres  24038  tsmsf1o  24039  tsmsxplem1  24047  tsmsxp  24049  isust  24098  ustssel  24100  ustincl  24102  ustdiag  24103  ustinvel  24104  ustexhalf  24105  ustexsym  24110  ust0  24114  restutop  24132  ustuqtop4  24139  utopsnneiplem  24142  blssexps  24321  blssex  24322  neibl  24396  blcld  24400  met1stc  24416  met2ndci  24417  metrest  24419  prdsxmslem2  24424  metustfbas  24452  cfilucfil  24454  metuel2  24460  metustbl  24461  restmetu  24465  dscopn  24468  isngp2  24492  tgioo  24691  tgqioo  24695  zdis  24712  xrge0tsms  24730  fsumcn  24768  volivth  25515  vitalilem2  25517  itgfsum  25735  limcun  25803  recnprss  25812  dvmptfsum  25886  ftc1a  25951  plyssc  26112  efopn  26574  jensen  26906  brsslt  27704  madef  27771  tglnunirn  28482  lpvtx  29002  umgredgprv  29041  usgredgprvALT  29129  issubgr2  29206  subgrprop2  29208  egrsubgr  29211  0uhgrsubgr  29213  frcond3  30205  hhsssh  31205  shintcl  31266  chintcl  31268  spanval  31269  omlsi  31340  pjoml  31372  chnlen0  31380  chsscon3  31436  chlejb1  31448  chnle  31450  spanun  31481  h1datom  31518  cmbr4i  31537  pjoml2  31547  pjoml3  31548  lecm  31553  osumcor2i  31580  osum  31581  spansncv  31589  pjcjt2  31628  pjopyth  31656  hstel2  32155  stj  32171  stcltr1i  32210  mdi  32231  mdbr3  32233  mdbr4  32234  dmdbr  32235  dmdmd  32236  dmdbr5  32244  mdsl1i  32257  mdslmd1lem3  32263  mdslmd1lem4  32264  mdslmd1i  32265  csmdsymi  32270  atss  32282  atom1d  32289  superpos  32290  chcv1  32291  shatomici  32294  shatomistici  32297  hatomistici  32298  chrelat2  32306  chirredi  32330  atcvat4i  32333  mdsymlem2  32340  mdsymlem6  32344  dmdbr6ati  32359  dmdbr7ati  32360  xrge0tsmsd  33009  gsumle  33045  gsumvsca1  33186  gsumvsca2  33187  prmidl  33418  ismxidl  33440  constrfiss  33748  zarcls1  33866  zarclsun  33867  zarclsiin  33868  zarclsint  33869  zarclssn  33870  zartop  33873  zartopon  33874  zart0  33876  zarmxt1  33877  zarcmp  33879  rhmpreimacnlem  33881  rhmpreimacn  33882  tpr2rico  33909  issiga  34109  isrnsiga  34110  sigagenval  34137  measiuns  34214  dya2icoseg  34275  dya2iocnrect  34279  dya2iocuni  34281  carsgmon  34312  carsgsigalem  34313  carsgclctunlem2  34317  carsgclctun  34319  pmeasmono  34322  pmeasadd  34323  bnj517  34882  bnj1118  34981  bnj1145  34990  bnj1154  34996  bnj1452  35049  bnj1498  35058  fineqvpow  35093  fineqvac  35094  fineqvacALT  35095  vonf1owev  35102  pthhashvtx  35122  kur14lem1  35200  cvmopnlem  35272  dfon2lem3  35780  dfon2lem7  35784  brsset  35884  fness  36344  fneref  36345  fnessref  36352  neibastop2lem  36355  topmeet  36359  fnejoin2  36364  tailfb  36372  filnetlem4  36376  onsucsuccmpi  36438  bj-snglss  36965  bj-elpwgALT  37049  bj-restpw  37087  bj-imdirco  37185  dissneqlem  37335  relowlssretop  37358  relowlpssretop  37359  ctbssinf  37401  pibt2  37412  matunitlindflem1  37617  ptrecube  37621  poimirlem29  37650  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  indexa  37734  indexdom  37735  neificl  37754  istotbnd3  37772  sstotbnd2  37775  sstotbnd  37776  equivtotbnd  37779  ssbnd  37789  heiborlem1  37812  heiborlem6  37817  heiborlem8  37819  heiborlem10  37821  unichnidl  38032  pridl  38038  ismaxidl  38041  igenval  38062  igenval2  38067  ispridlc  38071  relcnveq3  38316  iss2  38333  elrelscnveq3  38489  brssr  38499  lsmsat  39008  lssatomic  39011  lssats  39012  lsat0cv  39033  lcvexchlem4  39037  lcvexchlem5  39038  lsatcvatlem  39049  l1cvpat  39054  ispsubsp  39746  linepsubN  39753  pclvalN  39891  ispsubclN  39938  ispsubcl2N  39948  pclfinclN  39951  diaelrnN  41046  docavalN  41124  dochval  41352  dvh4dimat  41439  dochexmidlem1  41461  lpolconN  41488  mapdordlem2  41638  eqresfnbd  42227  ismrcd1  42693  ismrcd2  42694  ismrc  42696  mzpcompact2lem  42746  aomclem6  43055  hbtlem6  43125  onintunirab  43223  rp-brsslt  43419  ssficl  43565  ssuncl  43566  ssdifcl  43567  sssymdifcl  43568  elmapintrab  43572  clcnvlem  43619  iunrelexpmin1  43704  iunrelexpmin2  43708  clsk3nimkb  44036  clsk1indlem1  44041  isotone1  44044  isotone2  44045  ntrclsiso  44063  gneispace  44130  gneispacess2  44142  onfrALTlem5  44539  onfrALTlem5VD  44881  relpfrlem  44950  modelaxreplem1  44975  islptre  45624  dvmptconst  45920  dvmptidg  45922  dvmulcncf  45930  dvdivcncf  45932  dvmptfprod  45950  stoweidlem51  46056  stoweidlem52  46057  fourierdlem103  46214  fourierdlem104  46215  ioorrnopnlem  46309  ioorrnopnxrlem  46311  salgenval  46326  ovnval2  46550  ovncvrrp  46569  ovnsubaddlem1  46575  ovnsubadd  46577  ovncvr2  46616  hspmbl  46634  elsetpreimafvssdm  47391  isubgredg  47870  uhgrimisgrgriclem  47934  grimedg  47939  grtrissvtx  47947  grtrimap  47951  stgredgiun  47961  isubgr3stgrlem6  47974  isubgr3stgrlem7  47975  uspgrlimlem1  47991  uspgrlimlem2  47992  uspgrlimlem3  47993  uspgrlimlem4  47994  grlimgrtrilem1  47997  grlimgrtrilem2  47998  grlimgrtri  47999  usgrexmpl1lem  48016  usgrexmpl2lem  48021  uspgrsprfo  48140  unilbss  48810  sepfsepc  48920  unilbeu  48977  ipolubdm  48979  ipoglbdm  48982  discsubc  49057  iinfconstbas  49059  setrec1lem1  49680  setrec1lem4  49683  setrec2fun  49685  elsetrecslem  49692  elpglem2  49705