Theorem sseq1 3964

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  sseq12  3966  sseq1i  3967  sseq1d  3970  nssne2  4002  psseq1  4046  uneqdifeq  4449  sbss  4477  pwjust  4559  elpwg  4561  pwpw0  4774  sssn  4787  ssunsn2  4788  unimax  4906  trss  5222  al0ssb  5263  sseliALT  5264  elssabg  5304  intabs  5310  vpwex  5339  nnullss  5434  exss  5435  releq  5754  iss  6028  relcnvtrg  6258  fununi  6600  ssimaex  6956  isofrlem  7328  onssmin  7779  tfis  7839  tfisi  7843  funcnvuni  7917  ffoss  7931  f1oweALT  7957  frxp  8110  frxp2  8128  frrlem1  8271  frrlem13  8283  tfrlem1  8350  oawordeu  8528  coflton  8645  cofon1  8646  cofon2  8647  naddunif  8668  qsss  8761  boxcutc  8927  sbthlem2  9064  sbth  9073  findcard2d  9139  ssfi  9145  sbthfi  9171  php  9179  isinf  9213  unbnn2  9245  domunfican  9269  fiint  9274  finsschain  9304  indexfi  9305  dffi3  9379  hartogslem1  9492  cantnfval2  9626  cantnfle  9628  cantnflem1  9646  tz9.1  9686  tcvalg  9693  setind  9704  frmin  9709  scott0  9848  bnd2  9867  carduni  9955  cardaleph  10061  alephinit  10067  aceq3lem  10092  dfac12lem3  10117  infmap2  10188  cflem  10216  cflemOLD  10217  cflm  10221  cflecard  10224  cfeq0  10228  cfsuc  10229  cfflb  10231  cfslb  10238  cfslb2n  10240  coftr  10245  fin23lem13  10304  fin23lem16  10307  fin23lem19  10308  fin23lem29  10313  fin1a2lem13  10384  itunitc  10393  domtriomlem  10414  axdc3lem2  10423  zorn2lem7  10474  zornn0g  10477  pwfseqlem4a  10634  pwfseqlem4  10635  wunfi  10694  wunex2  10711  wuncval  10715  rankcf  10750  tskuni  10756  axgroth6  10801  axgroth3  10804  axgroth4  10805  fzoss1  13706  fsuppmapnn0fiubex  14019  hashf1lem2  14483  cleq1lem  15009  rtrclreclem4  15088  sumeq1  15730  fsumcvg3  15770  fsum2d  15812  fsumabs  15843  fsumrlim  15853  fsumo1  15854  fsumiun  15863  prodeq1f  15950  prodeq1  15951  fprod2d  16025  lcmfunsnlem  16689  coprmprod  16709  vdwmc  17028  prmgaplem3  17103  prmgaplem4  17104  restsspw  17474  ismred2  17645  mrcval  17656  mrcuni  17667  acsfn  17705  isssc  17867  drsdirfi  18351  ipodrsima  18587  cntzssv  19389  pmtrfrn  19519  pmtrrn2  19521  pmtrdifellem1  19537  pmtrdifellem2  19538  sylow2alem2  19679  sylow2a  19680  efgval  19778  gsumzaddlem  19982  ablfac1eulem  20135  gsumle  20206  rgspnval  20688  lspval  21065  lspindpi  21225  unichnlidl  21331  prmidl  21427  znf1o  21661  zntoslem  21666  aspval  21982  mplsubglem  22108  mpllsslem  22109  mplcoe1  22148  mplcoe5  22151  mdetunilem9  22738  uniopn  23015  fiinopn  23019  fiinbas  23070  baspartn  23072  eltg2  23076  eltg3  23080  topbas  23090  pptbas  23126  clsval  23155  neiint  23222  neips  23231  opnneissb  23232  opnssneib  23233  innei  23243  neiptoptop  23249  neiptopnei  23250  restbas  23276  restcld  23290  neitr  23298  restcls  23299  restntr  23300  cnpdis  23411  cmpsublem  23517  cmpsub  23518  fiuncmp  23522  unconn  23547  1stcfb  23563  2ndc1stc  23569  1stcrest  23571  2ndcctbss  23573  2ndcomap  23576  dis2ndc  23578  lly1stc  23614  refssex  23629  refun0  23633  llycmpkgen2  23668  txbas  23685  eltx  23686  ptuni2  23694  neitx  23725  ptpjopn  23730  ptcld  23731  txlm  23766  tx1stc  23768  txkgen  23770  xkopt  23773  xkococnlem  23777  ptcmpfi  23931  fbssfi  23955  opnfbas  23960  isfil2  23974  isfildlem  23975  snfil  23982  fsubbas  23985  ssfg  23990  fgss2  23992  fgcl  23996  fbasrn  24002  fgtr  24008  ufli  24032  uffix  24039  rnelfmlem  24070  fclscf  24143  alexsublem  24162  alexsubALTlem2  24166  alexsubALTlem3  24167  alexsubALTlem4  24168  alexsubALT  24169  tmdgsum2  24214  subgntr  24225  opnsubg  24226  qustgpopn  24238  tsmsfbas  24246  tsmsgsum  24257  tsmsres  24262  tsmsf1o  24263  tsmsxplem1  24271  tsmsxp  24273  isust  24322  ustssel  24324  ustincl  24326  ustdiag  24327  ustinvel  24328  ustexhalf  24329  ustexsym  24334  ust0  24338  restutop  24355  ustuqtop4  24362  utopsnneiplem  24365  blssexps  24544  blssex  24545  neibl  24619  blcld  24623  met1stc  24639  met2ndci  24640  metrest  24642  prdsxmslem2  24647  metustfbas  24675  cfilucfil  24677  metuel2  24683  metustbl  24684  restmetu  24688  dscopn  24691  isngp2  24715  tgioo  24914  tgqioo  24918  zdis  24935  xrge0tsms  24953  fsumcn  24990  volivth  25727  vitalilem2  25729  itgfsum  25947  limcun  26015  recnprss  26024  dvmptfsum  26095  ftc1a  26157  plyssc  26318  efopn  26781  jensen  27111  brslts  27913  madef  27987  tglnunirn  28775  brprlng  29123  lpvtx  29327  umgredgprv  29366  usgredgprvALT  29454  issubgr2  29531  subgrprop2  29533  egrsubgr  29536  0uhgrsubgr  29538  frcond3  30529  hhsssh  31530  shintcl  31591  chintcl  31593  spanval  31594  omlsi  31665  pjoml  31697  chnlen0  31705  chsscon3  31761  chlejb1  31773  chnle  31775  spanun  31806  h1datom  31843  cmbr4i  31862  pjoml2  31872  pjoml3  31873  lecm  31878  osumcor2i  31905  osum  31906  spansncv  31914  pjcjt2  31953  pjopyth  31981  hstel2  32480  stj  32496  stcltr1i  32535  mdi  32556  mdbr3  32558  mdbr4  32559  dmdbr  32560  dmdmd  32561  dmdbr5  32569  mdsl1i  32582  mdslmd1lem3  32588  mdslmd1lem4  32589  mdslmd1i  32590  csmdsymi  32595  atss  32607  atom1d  32614  superpos  32615  chcv1  32616  shatomici  32619  shatomistici  32622  hatomistici  32623  chrelat2  32631  chirredi  32655  atcvat4i  32658  mdsymlem2  32665  mdsymlem6  32669  dmdbr6ati  32684  dmdbr7ati  32685  xrge0tsmsd  33306  gsumvsca1  33459  gsumvsca2  33460  ismxidl  33662  constrfiss  34058  zarcls1  34176  zarclsun  34177  zarclsiin  34178  zarclsint  34179  zarclssn  34180  zartop  34183  zartopon  34184  zart0  34186  zarmxt1  34187  zarcmp  34189  rhmpreimacnlem  34191  rhmpreimacn  34192  tpr2rico  34219  issiga  34419  isrnsiga  34420  sigagenval  34447  measiuns  34524  dya2icoseg  34584  dya2iocnrect  34588  dya2iocuni  34590  carsgmon  34621  carsgsigalem  34622  carsgclctunlem2  34626  carsgclctun  34628  pmeasmono  34631  pmeasadd  34632  bnj517  35190  bnj1118  35289  bnj1145  35298  bnj1154  35304  bnj1452  35357  bnj1498  35366  fineqvpow  35423  fineqvac  35424  fineqvacALT  35425  setindregs  35438  tz9.1regs  35442  fineqvr1ombregs  35446  vonf1wev  35463  vonf1owevOLD  35465  pthhashvtx  35491  kur14lem1  35569  cvmopnlem  35641  dfon2lem3  36146  dfon2lem7  36150  brsset  36250  fness  36722  fneref  36723  fnessref  36730  neibastop2lem  36733  topmeet  36737  fnejoin2  36742  tailfb  36750  filnetlem4  36754  onsucsuccmpi  36816  ttcwf2  36898  ttcexg  36905  bj-snglss  37467  bj-elpwgALT  37551  bj-restpw  37594  bj-imdirco  37694  dissneqlem  37846  relowlssretop  37869  relowlpssretop  37870  ctbssinf  37912  pibt2  37923  matunitlindflem1  38127  ptrecube  38131  poimirlem29  38160  mblfinlem2  38169  mblfinlem3  38170  mblfinlem4  38171  ismblfin  38172  ovoliunnfl  38173  voliunnfl  38175  volsupnfl  38176  indexa  38244  indexdom  38245  neificl  38264  istotbnd3  38282  sstotbnd2  38285  sstotbnd  38286  equivtotbnd  38289  ssbnd  38299  heiborlem1  38322  heiborlem6  38327  heiborlem8  38329  heiborlem10  38331  unichnidl  38542  pridl  38548  ismaxidl  38551  igenval  38572  igenval2  38577  ispridlc  38581  relcnveq3  38838  iss2  38855  brssr  39092  elrelscnveq3  39138  lsmsat  39644  lssatomic  39647  lssats  39648  lsat0cv  39669  lcvexchlem4  39673  lcvexchlem5  39674  lsatcvatlem  39685  l1cvpat  39690  ispsubsp  40381  linepsubN  40388  pclvalN  40526  ispsubclN  40573  ispsubcl2N  40583  pclfinclN  40586  diaelrnN  41681  docavalN  41759  dochval  41987  dvh4dimat  42074  dochexmidlem1  42096  lpolconN  42123  mapdordlem2  42273  eqresfnbd  42863  ismrcd1  43291  ismrcd2  43292  ismrc  43294  mzpcompact2lem  43344  aomclem6  43648  hbtlem6  43718  onintunirab  43816  rp-brsslt  44011  ssficl  44157  ssuncl  44158  ssdifcl  44159  sssymdifcl  44160  elmapintrab  44164  clcnvlem  44211  iunrelexpmin1  44296  iunrelexpmin2  44300  clsk3nimkb  44628  clsk1indlem1  44633  isotone1  44636  isotone2  44637  ntrclsiso  44655  gneispace  44722  gneispacess2  44734  onfrALTlem5  45116  onfrALTlem5VD  45458  relpfrlem  45527  modelaxreplem1  45552  islptre  46193  dvmptconst  46487  dvmptidg  46489  dvmulcncf  46497  dvdivcncf  46499  dvmptfprod  46517  stoweidlem51  46623  stoweidlem52  46624  fourierdlem103  46781  fourierdlem104  46782  ioorrnopnlem  46876  ioorrnopnxrlem  46878  salgenval  46893  ovnval2  47117  ovncvrrp  47136  ovnsubaddlem1  47142  ovnsubadd  47144  ovncvr2  47183  hspmbl  47201  elsetpreimafvssdm  47990  isubgredg  48486  uhgrimisgrgriclem  48550  grimedg  48555  grtrissvtx  48564  grtrimap  48568  stgredgiun  48578  isubgr3stgrlem6  48591  isubgr3stgrlem7  48592  uspgrlimlem1  48608  uspgrlimlem2  48609  uspgrlimlem3  48610  uspgrlimlem4  48611  clnbgrvtxedg  48614  grlimedgclnbgr  48615  grlimpredg  48618  grlimprclnbgrvtx  48619  grlimgredgex  48620  grlimgrtrilem1  48621  grlimgrtrilem2  48622  grlimgrtri  48623  usgrexmpl1lem  48641  usgrexmpl2lem  48646  uspgrsprfo  48768  unilbss  49447  sepfsepc  49557  unilbeu  49614  ipolubdm  49616  ipoglbdm  49619  discsubc  49693  iinfconstbas  49695  setrec1lem1  50316  setrec1lem4  50319  setrec2fun  50321  elsetrecslem  50328  elpglem2  50341