Theorem sseq1 3961

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 3951	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3942	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3942	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	2, 3	anbiim 642	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
5	4	ancoms 458	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
6	1, 5	sylbi 217	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  sseq12  3963  sseq1i  3964  sseq1d  3967  nssne2  3999  psseq1  4044  uneqdifeq  4447  sbss  4475  pwjust  4557  elpwg  4559  pwpw0  4771  sssn  4784  ssunsn2  4785  unimax  4902  trss  5217  al0ssb  5255  sseliALT  5256  elssabg  5290  intabs  5296  vpwex  5324  nnullss  5417  exss  5418  releq  5734  iss  6002  relcnvtrg  6233  fununi  6575  ssimaex  6927  isofrlem  7296  onssmin  7747  tfis  7807  tfisi  7811  funcnvuni  7884  ffoss  7900  f1oweALT  7926  frxp  8078  frxp2  8096  frrlem1  8238  frrlem13  8250  tfrlem1  8317  oawordeu  8492  coflton  8609  cofon1  8610  cofon2  8611  naddunif  8631  qsss  8724  boxcutc  8891  sbthlem2  9028  sbth  9037  findcard2d  9103  ssfi  9109  sbthfi  9135  php  9143  isinf  9177  unbnn2  9209  domunfican  9234  fiint  9239  finsschain  9271  indexfi  9272  dffi3  9346  hartogslem1  9459  cantnfval2  9590  cantnfle  9592  cantnflem1  9610  tz9.1  9650  tcvalg  9657  setind  9668  frmin  9673  scott0  9810  bnd2  9817  carduni  9905  cardaleph  10011  alephinit  10017  aceq3lem  10042  dfac12lem3  10068  infmap2  10139  cflem  10167  cflemOLD  10168  cflm  10172  cflecard  10175  cfeq0  10178  cfsuc  10179  cfflb  10181  cfslb  10188  cfslb2n  10190  coftr  10195  fin23lem13  10254  fin23lem16  10257  fin23lem19  10258  fin23lem29  10263  fin1a2lem13  10334  itunitc  10343  domtriomlem  10364  axdc3lem2  10373  zorn2lem7  10424  zornn0g  10427  pwfseqlem4a  10584  pwfseqlem4  10585  wunfi  10644  wunex2  10661  wuncval  10665  rankcf  10700  tskuni  10706  axgroth6  10751  axgroth3  10754  axgroth4  10755  fzoss1  13614  fsuppmapnn0fiubex  13927  hashf1lem2  14391  cleq1lem  14917  rtrclreclem4  14996  sumeq1  15624  fsumcvg3  15664  fsum2d  15706  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  prodeq1f  15841  prodeq1  15842  fprod2d  15916  lcmfunsnlem  16580  coprmprod  16600  vdwmc  16918  prmgaplem3  16993  prmgaplem4  16994  restsspw  17363  ismred2  17534  mrcval  17545  mrcuni  17556  acsfn  17594  isssc  17756  drsdirfi  18240  ipodrsima  18476  cntzssv  19269  pmtrfrn  19399  pmtrrn2  19401  pmtrdifellem1  19417  pmtrdifellem2  19418  sylow2alem2  19559  sylow2a  19560  efgval  19658  gsumzaddlem  19862  ablfac1eulem  20015  gsumle  20086  rgspnval  20557  lspval  20938  lspindpi  21099  znf1o  21518  zntoslem  21523  aspval  21840  mplsubglem  21966  mpllsslem  21967  mplcoe1  22004  mplcoe5  22007  mdetunilem9  22576  uniopn  22853  fiinopn  22857  fiinbas  22908  baspartn  22910  eltg2  22914  eltg3  22918  topbas  22928  pptbas  22964  clsval  22993  neiint  23060  neips  23069  opnneissb  23070  opnssneib  23071  innei  23081  neiptoptop  23087  neiptopnei  23088  restbas  23114  restcld  23128  neitr  23136  restcls  23137  restntr  23138  cnpdis  23249  cmpsublem  23355  cmpsub  23356  fiuncmp  23360  unconn  23385  1stcfb  23401  2ndc1stc  23407  1stcrest  23409  2ndcctbss  23411  2ndcomap  23414  dis2ndc  23416  lly1stc  23452  refssex  23467  refun0  23471  llycmpkgen2  23506  txbas  23523  eltx  23524  ptuni2  23532  neitx  23563  ptpjopn  23568  ptcld  23569  txlm  23604  tx1stc  23606  txkgen  23608  xkopt  23611  xkococnlem  23615  ptcmpfi  23769  fbssfi  23793  opnfbas  23798  isfil2  23812  isfildlem  23813  snfil  23820  fsubbas  23823  ssfg  23828  fgss2  23830  fgcl  23834  fbasrn  23840  fgtr  23846  ufli  23870  uffix  23877  rnelfmlem  23908  fclscf  23981  alexsublem  24000  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  alexsubALT  24007  tmdgsum2  24052  subgntr  24063  opnsubg  24064  qustgpopn  24076  tsmsfbas  24084  tsmsgsum  24095  tsmsres  24100  tsmsf1o  24101  tsmsxplem1  24109  tsmsxp  24111  isust  24160  ustssel  24162  ustincl  24164  ustdiag  24165  ustinvel  24166  ustexhalf  24167  ustexsym  24172  ust0  24176  restutop  24193  ustuqtop4  24200  utopsnneiplem  24203  blssexps  24382  blssex  24383  neibl  24457  blcld  24461  met1stc  24477  met2ndci  24478  metrest  24480  prdsxmslem2  24485  metustfbas  24513  cfilucfil  24515  metuel2  24521  metustbl  24522  restmetu  24526  dscopn  24529  isngp2  24553  tgioo  24752  tgqioo  24756  zdis  24773  xrge0tsms  24791  fsumcn  24829  volivth  25576  vitalilem2  25578  itgfsum  25796  limcun  25864  recnprss  25873  dvmptfsum  25947  ftc1a  26012  plyssc  26173  efopn  26635  jensen  26967  brslts  27770  madef  27844  tglnunirn  28632  lpvtx  29153  umgredgprv  29192  usgredgprvALT  29280  issubgr2  29357  subgrprop2  29359  egrsubgr  29362  0uhgrsubgr  29364  frcond3  30356  hhsssh  31356  shintcl  31417  chintcl  31419  spanval  31420  omlsi  31491  pjoml  31523  chnlen0  31531  chsscon3  31587  chlejb1  31599  chnle  31601  spanun  31632  h1datom  31669  cmbr4i  31688  pjoml2  31698  pjoml3  31699  lecm  31704  osumcor2i  31731  osum  31732  spansncv  31740  pjcjt2  31779  pjopyth  31807  hstel2  32306  stj  32322  stcltr1i  32361  mdi  32382  mdbr3  32384  mdbr4  32385  dmdbr  32386  dmdmd  32387  dmdbr5  32395  mdsl1i  32408  mdslmd1lem3  32414  mdslmd1lem4  32415  mdslmd1i  32416  csmdsymi  32421  atss  32433  atom1d  32440  superpos  32441  chcv1  32442  shatomici  32445  shatomistici  32448  hatomistici  32449  chrelat2  32457  chirredi  32481  atcvat4i  32484  mdsymlem2  32491  mdsymlem6  32495  dmdbr6ati  32510  dmdbr7ati  32511  xrge0tsmsd  33166  gsumvsca1  33319  gsumvsca2  33320  prmidl  33532  ismxidl  33554  constrfiss  33928  zarcls1  34046  zarclsun  34047  zarclsiin  34048  zarclsint  34049  zarclssn  34050  zartop  34053  zartopon  34054  zart0  34056  zarmxt1  34057  zarcmp  34059  rhmpreimacnlem  34061  rhmpreimacn  34062  tpr2rico  34089  issiga  34289  isrnsiga  34290  sigagenval  34317  measiuns  34394  dya2icoseg  34454  dya2iocnrect  34458  dya2iocuni  34460  carsgmon  34491  carsgsigalem  34492  carsgclctunlem2  34496  carsgclctun  34498  pmeasmono  34501  pmeasadd  34502  bnj517  35060  bnj1118  35159  bnj1145  35168  bnj1154  35174  bnj1452  35227  bnj1498  35236  fineqvpow  35290  fineqvac  35291  fineqvacALT  35292  setindregs  35305  tz9.1regs  35309  fineqvr1ombregs  35313  vonf1owev  35321  pthhashvtx  35341  kur14lem1  35419  cvmopnlem  35491  dfon2lem3  35996  dfon2lem7  36000  brsset  36100  fness  36562  fneref  36563  fnessref  36570  neibastop2lem  36573  topmeet  36577  fnejoin2  36582  tailfb  36590  filnetlem4  36594  onsucsuccmpi  36656  bj-snglss  37212  bj-elpwgALT  37296  bj-restpw  37339  bj-imdirco  37439  dissneqlem  37589  relowlssretop  37612  relowlpssretop  37613  ctbssinf  37655  pibt2  37666  matunitlindflem1  37861  ptrecube  37865  poimirlem29  37894  mblfinlem2  37903  mblfinlem3  37904  mblfinlem4  37905  ismblfin  37906  ovoliunnfl  37907  voliunnfl  37909  volsupnfl  37910  indexa  37978  indexdom  37979  neificl  37998  istotbnd3  38016  sstotbnd2  38019  sstotbnd  38020  equivtotbnd  38023  ssbnd  38033  heiborlem1  38056  heiborlem6  38061  heiborlem8  38063  heiborlem10  38065  unichnidl  38276  pridl  38282  ismaxidl  38285  igenval  38306  igenval2  38311  ispridlc  38315  relcnveq3  38572  iss2  38589  brssr  38826  elrelscnveq3  38872  lsmsat  39378  lssatomic  39381  lssats  39382  lsat0cv  39403  lcvexchlem4  39407  lcvexchlem5  39408  lsatcvatlem  39419  l1cvpat  39424  ispsubsp  40115  linepsubN  40122  pclvalN  40260  ispsubclN  40307  ispsubcl2N  40317  pclfinclN  40320  diaelrnN  41415  docavalN  41493  dochval  41721  dvh4dimat  41808  dochexmidlem1  41830  lpolconN  41857  mapdordlem2  42007  eqresfnbd  42598  ismrcd1  43049  ismrcd2  43050  ismrc  43052  mzpcompact2lem  43102  aomclem6  43410  hbtlem6  43480  onintunirab  43578  rp-brsslt  43773  ssficl  43919  ssuncl  43920  ssdifcl  43921  sssymdifcl  43922  elmapintrab  43926  clcnvlem  43973  iunrelexpmin1  44058  iunrelexpmin2  44062  clsk3nimkb  44390  clsk1indlem1  44395  isotone1  44398  isotone2  44399  ntrclsiso  44417  gneispace  44484  gneispacess2  44496  onfrALTlem5  44892  onfrALTlem5VD  45234  relpfrlem  45303  modelaxreplem1  45328  islptre  45973  dvmptconst  46267  dvmptidg  46269  dvmulcncf  46277  dvdivcncf  46279  dvmptfprod  46297  stoweidlem51  46403  stoweidlem52  46404  fourierdlem103  46561  fourierdlem104  46562  ioorrnopnlem  46656  ioorrnopnxrlem  46658  salgenval  46673  ovnval2  46897  ovncvrrp  46916  ovnsubaddlem1  46922  ovnsubadd  46924  ovncvr2  46963  hspmbl  46981  elsetpreimafvssdm  47740  isubgredg  48220  uhgrimisgrgriclem  48284  grimedg  48289  grtrissvtx  48298  grtrimap  48302  stgredgiun  48312  isubgr3stgrlem6  48325  isubgr3stgrlem7  48326  uspgrlimlem1  48342  uspgrlimlem2  48343  uspgrlimlem3  48344  uspgrlimlem4  48345  clnbgrvtxedg  48348  grlimedgclnbgr  48349  grlimpredg  48352  grlimprclnbgrvtx  48353  grlimgredgex  48354  grlimgrtrilem1  48355  grlimgrtrilem2  48356  grlimgrtri  48357  usgrexmpl1lem  48375  usgrexmpl2lem  48380  uspgrsprfo  48502  unilbss  49171  sepfsepc  49281  unilbeu  49338  ipolubdm  49340  ipoglbdm  49343  discsubc  49417  iinfconstbas  49419  setrec1lem1  50040  setrec1lem4  50043  setrec2fun  50045  elsetrecslem  50052  elpglem2  50065