Theorem sseq1 3938

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  sseq12  3940  sseq1i  3941  sseq1d  3944  nssne2  3976  psseq1  4020  vvin  4362  uneqdifeq  4451  sbss  4479  pwjust  4561  elpwg  4563  sssn  4785  ssunsn2  4786  pwpw0  4834  unimax  4908  trss  5225  al0ssb  5265  sseliALT  5266  elssabg  5308  intabs  5314  vpwex  5343  nnullss  5434  exss  5435  releq  5758  iss  6039  relcnvtrgOLD  6287  fununi  6637  ssimaex  6993  isofrlem  7371  onssmin  7830  tfis  7890  tfisi  7894  funcnvuni  7968  ffoss  7982  f1oweALT  8008  ovmptss  8129  frxp  8165  frxp2  8188  frrlem1  8332  frrlem13  8344  tfrlem1  8411  oawordeu  8591  coflton  8708  cofon1  8709  cofon2  8710  naddunif  8731  qsss  8824  boxcutc  8997  sbthlem2  9135  sbth  9144  findcard2d  9210  ssfi  9216  sbthfi  9242  php  9250  isinf  9284  unbnn2  9317  domunfican  9341  fiint  9346  finsschain  9376  indexfi  9377  dffi3  9450  hartogslem1  9563  cantnfval2  9697  cantnfle  9699  cantnflem1  9717  tz9.1  9757  tcvalg  9764  setind  9775  frmin  9780  scott0b  9964  scott0OLD  9965  bnd2  9983  setrec1lem1  9993  setrec1lem4  9998  setrec2fun  10000  carduni  10089  cardaleph  10195  alephinit  10201  aceq3lem  10226  dfac12lem3  10251  infmap2  10322  cflem  10350  cflm  10354  cflecard  10357  cfeq0  10361  cfsuc  10362  cfflb  10364  cfslb  10371  cfslb2n  10373  coftr  10378  fin23lem13  10437  fin23lem16  10440  fin23lem19  10441  fin23lem29  10446  fin1a2lem13  10517  itunitc  10526  domtriomlem  10547  axdc3lem2  10556  zorn2lem7  10607  zornn0g  10610  pwfseqlem4a  10773  pwfseqlem4  10774  wunfi  10833  wunex2  10850  wuncval  10854  rankcf  10889  tskuni  10895  axgroth6  10940  axgroth3  10943  axgroth4  10944  fzoss1  13848  fsuppmapnn0fiubex  14162  hashf1lem2  14628  cleq1lem  15164  rtrclreclem4  15243  sumeq1  15885  fsumcvg3  15924  fsum2d  15966  fsumabs  15997  fsumrlim  16007  fsumo1  16008  fsumiun  16017  prodeq1f  16104  prodeq1  16105  fprod2d  16177  lcmfunsnlem  16845  coprmprod  16865  vdwmc  17185  prmgaplem3  17260  prmgaplem4  17261  restsspw  17631  ismred2  17802  mrcval  17813  mrcuni  17824  acsfn  17862  isssc  18024  drsdirfi  18508  ipodrsima  18744  cntzssv  19572  pmtrfrn  19702  pmtrrn2  19704  pmtrdifellem1  19720  pmtrdifellem2  19721  sylow2alem2  19862  sylow2a  19863  efgval  19961  gsumzaddlem  20165  ablfac1eulem  20318  gsumle  20389  rgspnval  20894  lspval  21280  lspindpi  21440  unichnlidl  21546  rspprop  21554  prmidl  21651  znf1o  21887  zntoslem  21892  aspval  22210  mplsubglem  22336  mpllsslem  22337  mplcoe1  22376  mplcoe5  22379  mdetunilem9  22965  matunitlindflem1  23024  uniopn  23245  fiinopn  23249  fiinbas  23300  baspartn  23302  eltg2  23306  eltg3  23310  topbas  23320  pptbas  23356  clsval  23385  neiint  23452  neips  23461  opnneissb  23462  opnssneib  23463  innei  23473  neiptoptop  23479  neiptopnei  23480  restbas  23506  restcld  23520  neitr  23528  restcls  23529  restntr  23530  cnpdis  23641  cmpsublem  23747  cmpsub  23748  fiuncmp  23752  unconn  23777  1stcfb  23793  2ndc1stc  23799  1stcrest  23801  2ndcctbss  23804  2ndcomap  23807  dis2ndc  23809  lly1stc  23845  refssex  23860  refun0  23864  llycmpkgen2  23899  txbas  23916  eltx  23917  ptuni2  23925  neitx  23956  ptpjopn  23961  ptcld  23962  txlm  23997  tx1stc  23999  txkgen  24001  xkopt  24004  xkococnlem  24008  ptcmpfi  24162  fbssfi  24186  opnfbas  24191  isfil2  24205  isfildlem  24206  snfil  24213  fsubbas  24216  ssfg  24221  fgss2  24223  fgcl  24227  fbasrn  24233  fgtr  24239  ufli  24263  uffix  24270  rnelfmlem  24301  fclscf  24374  alexsublem  24393  alexsubALTlem2  24397  alexsubALTlem3  24398  alexsubALTlem4  24399  alexsubALT  24400  tmdgsum2  24445  subgntr  24456  opnsubg  24457  qustgpopn  24469  tsmsfbas  24477  tsmsgsum  24488  tsmsres  24493  tsmsf1o  24494  tsmsxplem1  24502  tsmsxp  24504  isust  24553  ustssel  24555  ustincl  24557  ustdiag  24558  ustinvel  24559  ustexhalf  24560  ustexsym  24565  ust0  24569  restutop  24586  ustuqtop4  24593  utopsnneiplem  24596  blssexps  24775  blssex  24776  neibl  24850  blcld  24854  met1stc  24870  met2ndci  24871  metrest  24873  prdsxmslem2  24878  metustfbas  24906  cfilucfil  24908  metuel2  24914  metustbl  24915  restmetu  24919  dscopn  24922  isngp2  24946  tgioo  25145  tgqioo  25149  zdis  25166  xrge0tsms  25184  fsumcn  25221  volivth  25958  vitalilem2  25960  itgfsum  26177  limcun  26245  recnprss  26254  dvmptfsum  26325  ftc1a  26387  plyssc  26548  efopn  27016  jensen  27346  brslts  28178  madef  28252  tglnunirn  29041  brprlng  29446  lpvtx  29676  umgredgprv  29715  usgredgprvALT  29806  issubgr2  29883  subgrprop2  29885  egrsubgr  29888  0uhgrsubgr  29890  pthhashvtx  30345  frcond3  30900  hhsssh  31901  shintcl  31962  chintcl  31964  spanval  31965  omlsi  32036  pjoml  32068  chnlen0  32076  chsscon3  32132  chlejb1  32144  chnle  32146  spanun  32177  h1datom  32214  cmbr4i  32233  pjoml2  32243  pjoml3  32244  lecm  32249  osumcor2i  32276  osum  32277  spansncv  32285  pjcjt2  32324  pjopyth  32352  hstel2  32851  stj  32867  stcltr1i  32906  mdi  32927  mdbr3  32929  mdbr4  32930  dmdbr  32931  dmdmd  32932  dmdbr5  32940  mdsl1i  32953  mdslmd1lem3  32959  mdslmd1lem4  32960  mdslmd1i  32961  csmdsymi  32966  atss  32978  atom1d  32985  superpos  32986  chcv1  32987  shatomici  32990  shatomistici  32993  hatomistici  32994  chrelat2  33002  chirredi  33026  atcvat4i  33029  mdsymlem2  33036  mdsymlem6  33040  dmdbr6ati  33055  dmdbr7ati  33056  xrge0tsmsd  33704  gsumvsca1  33857  gsumvsca2  33858  ismxidl  34057  constrfiss  34453  zarcls1  34571  zarclsun  34572  zarclsiin  34573  zarclsint  34574  zarclssn  34575  zartop  34578  zartopon  34579  zart0  34581  zarmxt1  34582  zarcmp  34584  rhmpreimacnlem  34586  rhmpreimacn  34587  tpr2rico  34614  issiga  34814  isrnsiga  34815  sigagenval  34843  measiuns  34920  dya2icoseg  34979  dya2iocnrect  34983  dya2iocuni  34985  carsgmon  35016  carsgsigalem  35017  carsgclctunlem2  35021  carsgclctun  35023  pmeasmono  35026  pmeasadd  35027  bnj517  35585  bnj1118  35684  bnj1145  35693  bnj1154  35699  bnj1452  35752  bnj1498  35761  rankscottu  35839  weexenwe  35848  acwer1prclem  35851  fineqvpow  35883  fineqvac  35884  fineqvacALT  35885  setindregs  35898  tz9.1regs  35902  fineqvhfbregs  35906  rankkardu  35939  vonf1wev  36036  vonf1owevOLD  36038  onprcf1acwevdlem1  36045  kur14lem1  36138  cvmopnlem  36210  dfon2lem3  36725  dfon2lem7  36729  brsset  36829  fness  37315  fneref  37316  fnessref  37323  neibastop2lem  37326  topmeet  37330  fnejoin2  37335  tailfb  37343  filnetlem4  37347  onsucsuccmpi  37409  ttcwf2  37491  ttcexg  37498  bj-snglss  38061  relssresv  38145  bj-elpwgALT  38160  bj-restpw  38204  bj-imdirco  38303  dissneqlem  38455  relowlssretop  38478  relowlpssretop  38479  ctbssinf  38521  pibt2  38532  ptrecube  38730  poimirlem29  38759  mblfinlem2  38768  mblfinlem3  38769  mblfinlem4  38770  ismblfin  38771  ovoliunnfl  38772  voliunnfl  38774  volsupnfl  38775  indexa  38859  indexdom  38860  neificl  38879  istotbnd3  38897  sstotbnd2  38900  sstotbnd  38901  equivtotbnd  38904  ssbnd  38914  heiborlem1  38937  heiborlem6  38942  heiborlem8  38944  heiborlem10  38946  unichnidl  39157  pridl  39163  ismaxidl  39166  igenval  39187  igenval2  39192  ispridlc  39196  relcnveq3  39451  iss2  39468  brssr  39705  elrelscnveq3  39751  lsmsat  40257  lssatomic  40260  lssats  40261  lsat0cv  40282  lcvexchlem4  40286  lcvexchlem5  40287  lsatcvatlem  40298  l1cvpat  40303  ispsubsp  40994  linepsubN  41001  pclvalN  41139  ispsubclN  41186  ispsubcl2N  41196  pclfinclN  41199  diaelrnN  42294  docavalN  42372  dochval  42600  dvh4dimat  42687  dochexmidlem1  42709  lpolconN  42736  mapdordlem2  42886  eqresfnbd  43479  ismrcd1  43902  ismrcd2  43903  ismrc  43905  mzpcompact2lem  43955  aomclem6  44254  hbtlem6  44323  onintunirab  44421  rp-brsslt  44616  ssficl  44762  ssuncl  44763  ssdifcl  44764  sssymdifcl  44765  elmapintrab  44769  clcnvlem  44815  iunrelexpmin1  44900  iunrelexpmin2  44904  clsk3nimkb  45232  clsk1indlem1  45237  isotone1  45240  isotone2  45241  ntrclsiso  45259  gneispace  45326  gneispacess2  45338  onfrALTlem5  45716  onfrALTlem5VD  46058  relpfrlem  46138  modelaxreplem1  46163  islptre  46836  dvmptconst  47130  dvmptidg  47132  dvmulcncf  47140  dvdivcncf  47142  dvmptfprod  47160  stoweidlem51  47266  stoweidlem52  47267  fourierdlem103  47424  fourierdlem104  47425  ioorrnopnlem  47519  ioorrnopnxrlem  47521  salgenval  47536  ovnval2  47760  ovncvrrp  47779  ovnsubaddlem1  47785  ovnsubadd  47787  ovncvr2  47826  hspmbl  47844  elsetpreimafvssdm  48673  isubgredg  49169  uhgrimisgrgriclem  49233  grimedg  49238  grtrissvtx  49247  grtrimap  49251  stgredgiun  49261  isubgr3stgrlem6  49274  isubgr3stgrlem7  49275  uspgrlimlem1  49291  uspgrlimlem2  49292  uspgrlimlem3  49293  uspgrlimlem4  49294  clnbgrvtxedg  49297  grlimedgclnbgr  49298  grlimpredg  49301  grlimprclnbgrvtx  49302  grlimgredgex  49303  grlimgrtrilem1  49304  grlimgrtrilem2  49305  grlimgrtri  49306  usgrexmpl1lem  49324  usgrexmpl2lem  49329  uspgrsprfo  49451  unilbss  50134  sepfsepc  50247  unilbeu  50304  ipolubdm  50306  ipoglbdm  50309  discsubc  50383  iinfconstbas  50385  elsetrecslem  51072  elpglem2  51085