Theorem sseq1 3933

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseq12  3935  sseq1i  3936  sseq1d  3939  nssne2  3971  psseq1  4017  vvin  4358  uneqdifeq  4447  sbss  4475  pwjust  4557  elpwg  4559  sssn  4781  ssunsn2  4782  pwpw0  4830  unimax  4904  trss  5221  al0ssb  5261  sseliALT  5262  elssabg  5303  intabs  5309  vpwex  5338  nnullss  5429  exss  5430  releq  5752  iss  6026  relcnvtrgOLD  6269  fununi  6615  ssimaex  6970  isofrlem  7348  onssmin  7806  tfis  7866  tfisi  7870  funcnvuni  7944  ffoss  7958  f1oweALT  7984  ovmptss  8104  frxp  8140  frxp2  8163  frrlem1  8307  frrlem13  8319  tfrlem1  8386  oawordeu  8566  coflton  8683  cofon1  8684  cofon2  8685  naddunif  8706  qsss  8799  boxcutc  8972  sbthlem2  9110  sbth  9119  findcard2d  9185  ssfi  9191  sbthfi  9217  php  9225  isinf  9259  unbnn2  9292  domunfican  9316  fiint  9321  finsschain  9351  indexfi  9352  dffi3  9426  hartogslem1  9539  cantnfval2  9673  cantnfle  9675  cantnflem1  9693  tz9.1  9733  tcvalg  9740  setind  9751  frmin  9756  scott0b  9940  scott0OLD  9941  bnd2  9959  setrec1lem1  9969  setrec1lem4  9974  setrec2fun  9976  carduni  10065  cardaleph  10171  alephinit  10177  aceq3lem  10202  dfac12lem3  10227  infmap2  10298  cflem  10326  cflm  10330  cflecard  10333  cfeq0  10337  cfsuc  10338  cfflb  10340  cfslb  10347  cfslb2n  10349  coftr  10354  fin23lem13  10413  fin23lem16  10416  fin23lem19  10417  fin23lem29  10422  fin1a2lem13  10493  itunitc  10502  domtriomlem  10523  axdc3lem2  10532  zorn2lem7  10583  zornn0g  10586  pwfseqlem4a  10749  pwfseqlem4  10750  wunfi  10809  wunex2  10826  wuncval  10830  rankcf  10865  tskuni  10871  axgroth6  10916  axgroth3  10919  axgroth4  10920  fzoss1  13824  fsuppmapnn0fiubex  14138  hashf1lem2  14604  cleq1lem  15140  rtrclreclem4  15219  sumeq1  15861  fsumcvg3  15900  fsum2d  15942  fsumabs  15973  fsumrlim  15983  fsumo1  15984  fsumiun  15993  prodeq1f  16080  prodeq1  16081  fprod2d  16153  lcmfunsnlem  16821  coprmprod  16841  vdwmc  17161  prmgaplem3  17236  prmgaplem4  17237  restsspw  17607  ismred2  17778  mrcval  17789  mrcuni  17800  acsfn  17838  isssc  18000  drsdirfi  18484  ipodrsima  18720  cntzssv  19547  pmtrfrn  19677  pmtrrn2  19679  pmtrdifellem1  19695  pmtrdifellem2  19696  sylow2alem2  19837  sylow2a  19838  efgval  19936  gsumzaddlem  20140  ablfac1eulem  20293  gsumle  20364  rgspnval  20869  lspval  21255  lspindpi  21415  unichnlidl  21521  rspprop  21529  prmidl  21626  znf1o  21862  zntoslem  21867  aspval  22185  mplsubglem  22311  mpllsslem  22312  mplcoe1  22351  mplcoe5  22354  mdetunilem9  22940  matunitlindflem1  22999  uniopn  23220  fiinopn  23224  fiinbas  23275  baspartn  23277  eltg2  23281  eltg3  23285  topbas  23295  pptbas  23331  clsval  23360  neiint  23427  neips  23436  opnneissb  23437  opnssneib  23438  innei  23448  neiptoptop  23454  neiptopnei  23455  restbas  23481  restcld  23495  neitr  23503  restcls  23504  restntr  23505  cnpdis  23616  cmpsublem  23722  cmpsub  23723  fiuncmp  23727  unconn  23752  1stcfb  23768  2ndc1stc  23774  1stcrest  23776  2ndcctbss  23779  2ndcomap  23782  dis2ndc  23784  lly1stc  23820  refssex  23835  refun0  23839  llycmpkgen2  23874  txbas  23891  eltx  23892  ptuni2  23900  neitx  23931  ptpjopn  23936  ptcld  23937  txlm  23972  tx1stc  23974  txkgen  23976  xkopt  23979  xkococnlem  23983  ptcmpfi  24137  fbssfi  24161  opnfbas  24166  isfil2  24180  isfildlem  24181  snfil  24188  fsubbas  24191  ssfg  24196  fgss2  24198  fgcl  24202  fbasrn  24208  fgtr  24214  ufli  24238  uffix  24245  rnelfmlem  24276  fclscf  24349  alexsublem  24368  alexsubALTlem2  24372  alexsubALTlem3  24373  alexsubALTlem4  24374  alexsubALT  24375  tmdgsum2  24420  subgntr  24431  opnsubg  24432  qustgpopn  24444  tsmsfbas  24452  tsmsgsum  24463  tsmsres  24468  tsmsf1o  24469  tsmsxplem1  24477  tsmsxp  24479  isust  24528  ustssel  24530  ustincl  24532  ustdiag  24533  ustinvel  24534  ustexhalf  24535  ustexsym  24540  ust0  24544  restutop  24561  ustuqtop4  24568  utopsnneiplem  24571  blssexps  24750  blssex  24751  neibl  24825  blcld  24829  met1stc  24845  met2ndci  24846  metrest  24848  prdsxmslem2  24853  metustfbas  24881  cfilucfil  24883  metuel2  24889  metustbl  24890  restmetu  24894  dscopn  24897  isngp2  24921  tgioo  25120  tgqioo  25124  zdis  25141  xrge0tsms  25159  fsumcn  25196  volivth  25933  vitalilem2  25935  itgfsum  26152  limcun  26220  recnprss  26229  dvmptfsum  26300  ftc1a  26362  plyssc  26523  efopn  26991  jensen  27321  brslts  28153  madef  28227  tglnunirn  29016  brprlng  29421  lpvtx  29651  umgredgprv  29690  usgredgprvALT  29781  issubgr2  29858  subgrprop2  29860  egrsubgr  29863  0uhgrsubgr  29865  pthhashvtx  30320  frcond3  30875  hhsssh  31876  shintcl  31937  chintcl  31939  spanval  31940  omlsi  32011  pjoml  32043  chnlen0  32051  chsscon3  32107  chlejb1  32119  chnle  32121  spanun  32152  h1datom  32189  cmbr4i  32208  pjoml2  32218  pjoml3  32219  lecm  32224  osumcor2i  32251  osum  32252  spansncv  32260  pjcjt2  32299  pjopyth  32327  hstel2  32826  stj  32842  stcltr1i  32881  mdi  32902  mdbr3  32904  mdbr4  32905  dmdbr  32906  dmdmd  32907  dmdbr5  32915  mdsl1i  32928  mdslmd1lem3  32934  mdslmd1lem4  32935  mdslmd1i  32936  csmdsymi  32941  atss  32953  atom1d  32960  superpos  32961  chcv1  32962  shatomici  32965  shatomistici  32968  hatomistici  32969  chrelat2  32977  chirredi  33001  atcvat4i  33004  mdsymlem2  33011  mdsymlem6  33015  dmdbr6ati  33030  dmdbr7ati  33031  xrge0tsmsd  33680  gsumvsca1  33833  gsumvsca2  33834  ismxidl  34033  constrfiss  34429  zarcls1  34547  zarclsun  34548  zarclsiin  34549  zarclsint  34550  zarclssn  34551  zartop  34554  zartopon  34555  zart0  34557  zarmxt1  34558  zarcmp  34560  rhmpreimacnlem  34562  rhmpreimacn  34563  tpr2rico  34590  issiga  34790  isrnsiga  34791  sigagenval  34819  measiuns  34896  dya2icoseg  34955  dya2iocnrect  34959  dya2iocuni  34961  carsgmon  34992  carsgsigalem  34993  carsgclctunlem2  34997  carsgclctun  34999  pmeasmono  35002  pmeasadd  35003  bnj517  35561  bnj1118  35660  bnj1145  35669  bnj1154  35675  bnj1452  35728  bnj1498  35737  rankscottu  35807  weexenwe  35812  acwer1prclem  35815  fineqvpow  35839  fineqvac  35840  fineqvacALT  35841  setindregs  35854  tz9.1regs  35858  fineqvr1ombregs  35862  rankkardu  35895  vonf1wev  35955  vonf1owevOLD  35957  onprcf1acwevdlem1  35964  kur14lem1  36057  cvmopnlem  36129  dfon2lem3  36639  dfon2lem7  36643  brsset  36743  fness  37229  fneref  37230  fnessref  37237  neibastop2lem  37240  topmeet  37244  fnejoin2  37249  tailfb  37257  filnetlem4  37261  onsucsuccmpi  37323  ttcwf2  37405  ttcexg  37412  bj-snglss  37975  bj-elpwgALT  38061  bj-restpw  38105  bj-imdirco  38204  dissneqlem  38356  relowlssretop  38379  relowlpssretop  38380  ctbssinf  38422  pibt2  38433  ptrecube  38631  poimirlem29  38660  mblfinlem2  38669  mblfinlem3  38670  mblfinlem4  38671  ismblfin  38672  ovoliunnfl  38673  voliunnfl  38675  volsupnfl  38676  indexa  38760  indexdom  38761  neificl  38780  istotbnd3  38798  sstotbnd2  38801  sstotbnd  38802  equivtotbnd  38805  ssbnd  38815  heiborlem1  38838  heiborlem6  38843  heiborlem8  38845  heiborlem10  38847  unichnidl  39058  pridl  39064  ismaxidl  39067  igenval  39088  igenval2  39093  ispridlc  39097  relcnveq3  39352  iss2  39369  brssr  39606  elrelscnveq3  39652  lsmsat  40158  lssatomic  40161  lssats  40162  lsat0cv  40183  lcvexchlem4  40187  lcvexchlem5  40188  lsatcvatlem  40199  l1cvpat  40204  ispsubsp  40895  linepsubN  40902  pclvalN  41040  ispsubclN  41087  ispsubcl2N  41097  pclfinclN  41100  diaelrnN  42195  docavalN  42273  dochval  42501  dvh4dimat  42588  dochexmidlem1  42610  lpolconN  42637  mapdordlem2  42787  eqresfnbd  43379  ismrcd1  43802  ismrcd2  43803  ismrc  43805  mzpcompact2lem  43855  aomclem6  44154  hbtlem6  44224  onintunirab  44322  rp-brsslt  44517  ssficl  44663  ssuncl  44664  ssdifcl  44665  sssymdifcl  44666  elmapintrab  44670  clcnvlem  44716  iunrelexpmin1  44801  iunrelexpmin2  44805  clsk3nimkb  45133  clsk1indlem1  45138  isotone1  45141  isotone2  45142  ntrclsiso  45160  gneispace  45227  gneispacess2  45239  onfrALTlem5  45618  onfrALTlem5VD  45960  relpfrlem  46036  modelaxreplem1  46061  islptre  46724  dvmptconst  47018  dvmptidg  47020  dvmulcncf  47028  dvdivcncf  47030  dvmptfprod  47048  stoweidlem51  47154  stoweidlem52  47155  fourierdlem103  47312  fourierdlem104  47313  ioorrnopnlem  47407  ioorrnopnxrlem  47409  salgenval  47424  ovnval2  47648  ovncvrrp  47667  ovnsubaddlem1  47673  ovnsubadd  47675  ovncvr2  47714  hspmbl  47732  elsetpreimafvssdm  48561  isubgredg  49057  uhgrimisgrgriclem  49121  grimedg  49126  grtrissvtx  49135  grtrimap  49139  stgredgiun  49149  isubgr3stgrlem6  49162  isubgr3stgrlem7  49163  uspgrlimlem1  49179  uspgrlimlem2  49180  uspgrlimlem3  49181  uspgrlimlem4  49182  clnbgrvtxedg  49185  grlimedgclnbgr  49186  grlimpredg  49189  grlimprclnbgrvtx  49190  grlimgredgex  49191  grlimgrtrilem1  49192  grlimgrtrilem2  49193  grlimgrtri  49194  usgrexmpl1lem  49212  usgrexmpl2lem  49217  uspgrsprfo  49339  unilbss  50022  sepfsepc  50135  unilbeu  50192  ipolubdm  50194  ipoglbdm  50197  discsubc  50271  iinfconstbas  50273  elsetrecslem  50960  elpglem2  50973