Theorem sseq1 3956

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 3946	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3938	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3938	. . . 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 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  sseq12  3958  sseq1i  3959  sseq1d  3962  nssne2  3994  psseq1  4038  vvin  4359  uneqdifeq  4448  sbss  4476  pwjust  4558  elpwg  4560  pwpw0  4774  sssn  4787  ssunsn2  4788  unimax  4905  trss  5222  al0ssb  5262  sseliALT  5263  elssabg  5304  intabs  5310  vpwex  5339  nnullss  5430  exss  5431  releq  5753  iss  6029  relcnvtrgOLD  6262  fununi  6607  ssimaex  6962  isofrlem  7340  onssmin  7795  tfis  7855  tfisi  7859  funcnvuni  7933  ffoss  7947  f1oweALT  7973  frxp  8127  frxp2  8145  frrlem1  8288  frrlem13  8300  tfrlem1  8367  oawordeu  8547  coflton  8664  cofon1  8665  cofon2  8666  naddunif  8687  qsss  8780  boxcutc  8953  sbthlem2  9091  sbth  9100  findcard2d  9166  ssfi  9172  sbthfi  9198  php  9206  isinf  9240  unbnn2  9273  domunfican  9297  fiint  9302  finsschain  9332  indexfi  9333  dffi3  9407  hartogslem1  9520  cantnfval2  9654  cantnfle  9656  cantnflem1  9674  tz9.1  9714  tcvalg  9721  setind  9732  frmin  9737  scott0b  9918  scott0OLD  9919  bnd2  9937  setrec1lem1  9947  setrec1lem4  9952  setrec2fun  9954  carduni  10043  cardaleph  10149  alephinit  10155  aceq3lem  10180  dfac12lem3  10205  infmap2  10276  cflem  10304  cflm  10308  cflecard  10311  cfeq0  10315  cfsuc  10316  cfflb  10318  cfslb  10325  cfslb2n  10327  coftr  10332  fin23lem13  10391  fin23lem16  10394  fin23lem19  10395  fin23lem29  10400  fin1a2lem13  10471  itunitc  10480  domtriomlem  10501  axdc3lem2  10510  zorn2lem7  10561  zornn0g  10564  pwfseqlem4a  10727  pwfseqlem4  10728  wunfi  10787  wunex2  10804  wuncval  10808  rankcf  10843  tskuni  10849  axgroth6  10894  axgroth3  10897  axgroth4  10898  fzoss1  13801  fsuppmapnn0fiubex  14115  hashf1lem2  14581  cleq1lem  15115  rtrclreclem4  15194  sumeq1  15836  fsumcvg3  15875  fsum2d  15917  fsumabs  15948  fsumrlim  15958  fsumo1  15959  fsumiun  15968  prodeq1f  16055  prodeq1  16056  fprod2d  16128  lcmfunsnlem  16796  coprmprod  16816  vdwmc  17136  prmgaplem3  17211  prmgaplem4  17212  restsspw  17582  ismred2  17753  mrcval  17764  mrcuni  17775  acsfn  17813  isssc  17975  drsdirfi  18459  ipodrsima  18695  cntzssv  19522  pmtrfrn  19652  pmtrrn2  19654  pmtrdifellem1  19670  pmtrdifellem2  19671  sylow2alem2  19812  sylow2a  19813  efgval  19911  gsumzaddlem  20115  ablfac1eulem  20268  gsumle  20339  rgspnval  20844  lspval  21230  lspindpi  21390  unichnlidl  21496  rspprop  21504  prmidl  21601  znf1o  21837  zntoslem  21842  aspval  22160  mplsubglem  22286  mpllsslem  22287  mplcoe1  22326  mplcoe5  22329  mdetunilem9  22915  matunitlindflem1  22974  uniopn  23195  fiinopn  23199  fiinbas  23250  baspartn  23252  eltg2  23256  eltg3  23260  topbas  23270  pptbas  23306  clsval  23335  neiint  23402  neips  23411  opnneissb  23412  opnssneib  23413  innei  23423  neiptoptop  23429  neiptopnei  23430  restbas  23456  restcld  23470  neitr  23478  restcls  23479  restntr  23480  cnpdis  23591  cmpsublem  23697  cmpsub  23698  fiuncmp  23702  unconn  23727  1stcfb  23743  2ndc1stc  23749  1stcrest  23751  2ndcctbss  23754  2ndcomap  23757  dis2ndc  23759  lly1stc  23795  refssex  23810  refun0  23814  llycmpkgen2  23849  txbas  23866  eltx  23867  ptuni2  23875  neitx  23906  ptpjopn  23911  ptcld  23912  txlm  23947  tx1stc  23949  txkgen  23951  xkopt  23954  xkococnlem  23958  ptcmpfi  24112  fbssfi  24136  opnfbas  24141  isfil2  24155  isfildlem  24156  snfil  24163  fsubbas  24166  ssfg  24171  fgss2  24173  fgcl  24177  fbasrn  24183  fgtr  24189  ufli  24213  uffix  24220  rnelfmlem  24251  fclscf  24324  alexsublem  24343  alexsubALTlem2  24347  alexsubALTlem3  24348  alexsubALTlem4  24349  alexsubALT  24350  tmdgsum2  24395  subgntr  24406  opnsubg  24407  qustgpopn  24419  tsmsfbas  24427  tsmsgsum  24438  tsmsres  24443  tsmsf1o  24444  tsmsxplem1  24452  tsmsxp  24454  isust  24503  ustssel  24505  ustincl  24507  ustdiag  24508  ustinvel  24509  ustexhalf  24510  ustexsym  24515  ust0  24519  restutop  24536  ustuqtop4  24543  utopsnneiplem  24546  blssexps  24725  blssex  24726  neibl  24800  blcld  24804  met1stc  24820  met2ndci  24821  metrest  24823  prdsxmslem2  24828  metustfbas  24856  cfilucfil  24858  metuel2  24864  metustbl  24865  restmetu  24869  dscopn  24872  isngp2  24896  tgioo  25095  tgqioo  25099  zdis  25116  xrge0tsms  25134  fsumcn  25171  volivth  25908  vitalilem2  25910  itgfsum  26127  limcun  26195  recnprss  26204  dvmptfsum  26275  ftc1a  26337  plyssc  26498  efopn  26968  jensen  27298  brslts  28130  madef  28204  tglnunirn  28993  brprlng  29398  lpvtx  29628  umgredgprv  29667  usgredgprvALT  29758  issubgr2  29835  subgrprop2  29837  egrsubgr  29840  0uhgrsubgr  29842  pthhashvtx  30297  frcond3  30852  hhsssh  31853  shintcl  31914  chintcl  31916  spanval  31917  omlsi  31988  pjoml  32020  chnlen0  32028  chsscon3  32084  chlejb1  32096  chnle  32098  spanun  32129  h1datom  32166  cmbr4i  32185  pjoml2  32195  pjoml3  32196  lecm  32201  osumcor2i  32228  osum  32229  spansncv  32237  pjcjt2  32276  pjopyth  32304  hstel2  32803  stj  32819  stcltr1i  32858  mdi  32879  mdbr3  32881  mdbr4  32882  dmdbr  32883  dmdmd  32884  dmdbr5  32892  mdsl1i  32905  mdslmd1lem3  32911  mdslmd1lem4  32912  mdslmd1i  32913  csmdsymi  32918  atss  32930  atom1d  32937  superpos  32938  chcv1  32939  shatomici  32942  shatomistici  32945  hatomistici  32946  chrelat2  32954  chirredi  32978  atcvat4i  32981  mdsymlem2  32988  mdsymlem6  32992  dmdbr6ati  33007  dmdbr7ati  33008  xrge0tsmsd  33616  gsumvsca1  33769  gsumvsca2  33770  ismxidl  33969  constrfiss  34365  zarcls1  34483  zarclsun  34484  zarclsiin  34485  zarclsint  34486  zarclssn  34487  zartop  34490  zartopon  34491  zart0  34493  zarmxt1  34494  zarcmp  34496  rhmpreimacnlem  34498  rhmpreimacn  34499  tpr2rico  34526  issiga  34726  isrnsiga  34727  sigagenval  34755  measiuns  34832  dya2icoseg  34892  dya2iocnrect  34896  dya2iocuni  34898  carsgmon  34929  carsgsigalem  34930  carsgclctunlem2  34934  carsgclctun  34936  pmeasmono  34939  pmeasadd  34940  bnj517  35498  bnj1118  35597  bnj1145  35606  bnj1154  35612  bnj1452  35665  bnj1498  35674  rankscottu  35731  fineqvpow  35756  fineqvac  35757  fineqvacALT  35758  setindregs  35771  tz9.1regs  35775  fineqvr1ombregs  35779  rankkardu  35812  vonf1wev  35860  vonf1owevOLD  35862  kur14lem1  35940  cvmopnlem  36012  dfon2lem3  36517  dfon2lem7  36521  brsset  36621  fness  37107  fneref  37108  fnessref  37115  neibastop2lem  37118  topmeet  37122  fnejoin2  37127  tailfb  37135  filnetlem4  37139  onsucsuccmpi  37201  ttcwf2  37283  ttcexg  37290  bj-snglss  37853  bj-elpwgALT  37937  bj-restpw  37981  bj-imdirco  38079  dissneqlem  38231  relowlssretop  38254  relowlpssretop  38255  ctbssinf  38297  pibt2  38308  ptrecube  38506  poimirlem29  38535  mblfinlem2  38544  mblfinlem3  38545  mblfinlem4  38546  ismblfin  38547  ovoliunnfl  38548  voliunnfl  38550  volsupnfl  38551  indexa  38635  indexdom  38636  neificl  38655  istotbnd3  38673  sstotbnd2  38676  sstotbnd  38677  equivtotbnd  38680  ssbnd  38690  heiborlem1  38713  heiborlem6  38718  heiborlem8  38720  heiborlem10  38722  unichnidl  38933  pridl  38939  ismaxidl  38942  igenval  38963  igenval2  38968  ispridlc  38972  relcnveq3  39227  iss2  39244  brssr  39481  elrelscnveq3  39527  lsmsat  40033  lssatomic  40036  lssats  40037  lsat0cv  40058  lcvexchlem4  40062  lcvexchlem5  40063  lsatcvatlem  40074  l1cvpat  40079  ispsubsp  40770  linepsubN  40777  pclvalN  40915  ispsubclN  40962  ispsubcl2N  40972  pclfinclN  40975  diaelrnN  42070  docavalN  42148  dochval  42376  dvh4dimat  42463  dochexmidlem1  42485  lpolconN  42512  mapdordlem2  42662  eqresfnbd  43254  ismrcd1  43662  ismrcd2  43663  ismrc  43665  mzpcompact2lem  43715  aomclem6  44019  hbtlem6  44089  onintunirab  44187  rp-brsslt  44382  ssficl  44528  ssuncl  44529  ssdifcl  44530  sssymdifcl  44531  elmapintrab  44535  clcnvlem  44582  iunrelexpmin1  44667  iunrelexpmin2  44671  clsk3nimkb  44999  clsk1indlem1  45004  isotone1  45007  isotone2  45008  ntrclsiso  45026  gneispace  45093  gneispacess2  45105  onfrALTlem5  45484  onfrALTlem5VD  45826  relpfrlem  45895  modelaxreplem1  45920  islptre  46575  dvmptconst  46869  dvmptidg  46871  dvmulcncf  46879  dvdivcncf  46881  dvmptfprod  46899  stoweidlem51  47005  stoweidlem52  47006  fourierdlem103  47163  fourierdlem104  47164  ioorrnopnlem  47258  ioorrnopnxrlem  47260  salgenval  47275  ovnval2  47499  ovncvrrp  47518  ovnsubaddlem1  47524  ovnsubadd  47526  ovncvr2  47565  hspmbl  47583  elsetpreimafvssdm  48412  isubgredg  48908  uhgrimisgrgriclem  48972  grimedg  48977  grtrissvtx  48986  grtrimap  48990  stgredgiun  49000  isubgr3stgrlem6  49013  isubgr3stgrlem7  49014  uspgrlimlem1  49030  uspgrlimlem2  49031  uspgrlimlem3  49032  uspgrlimlem4  49033  clnbgrvtxedg  49036  grlimedgclnbgr  49037  grlimpredg  49040  grlimprclnbgrvtx  49041  grlimgredgex  49042  grlimgrtrilem1  49043  grlimgrtrilem2  49044  grlimgrtri  49045  usgrexmpl1lem  49063  usgrexmpl2lem  49068  uspgrsprfo  49190  unilbss  49872  sepfsepc  49980  unilbeu  50037  ipolubdm  50039  ipoglbdm  50042  discsubc  50116  iinfconstbas  50118  elsetrecslem  50736  elpglem2  50749