Theorem sseq1 4009

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  sseq12  4011  sseq1i  4012  sseq1d  4015  nssne2  4047  psseq1  4090  uneqdifeq  4493  sbss  4519  pwjust  4601  elpwg  4603  pwpw0  4813  sssn  4826  ssunsn2  4827  unimax  4944  trss  5270  al0ssb  5308  sseliALT  5309  elssabg  5343  intabs  5349  vpwex  5377  nnullss  5467  exss  5468  friOLD  5643  releq  5786  iss  6053  relcnvtrg  6286  fununi  6641  ssimaex  6994  isofrlem  7360  onssmin  7812  tfis  7876  tfisi  7880  funcnvuni  7954  ffoss  7970  f1oweALT  7997  frxp  8151  frxp2  8169  frrlem1  8311  frrlem13  8323  wfrlem1OLD  8348  wfrlem4OLD  8352  wfrlem15OLD  8363  tfrlem1  8416  oawordeu  8593  coflton  8709  cofon1  8710  cofon2  8711  naddunif  8731  qsss  8818  boxcutc  8981  sbthlem2  9124  sbth  9133  findcard2d  9206  ssfi  9213  sbthfi  9239  php  9247  phpOLD  9259  isinf  9296  isinfOLD  9297  unbnn2  9333  domunfican  9361  fiint  9366  fiintOLD  9367  finsschain  9399  indexfi  9400  dffi3  9471  hartogslem1  9582  cantnfval2  9709  cantnfle  9711  cantnflem1  9729  tz9.1  9769  setind  9774  tcvalg  9778  frmin  9789  scott0  9926  bnd2  9933  carduni  10021  cardaleph  10129  alephinit  10135  aceq3lem  10160  dfac12lem3  10186  infmap2  10257  cflem  10285  cflemOLD  10286  cflm  10290  cflecard  10293  cfeq0  10296  cfsuc  10297  cfflb  10299  cfslb  10306  cfslb2n  10308  coftr  10313  fin23lem13  10372  fin23lem16  10375  fin23lem19  10376  fin23lem29  10381  fin1a2lem13  10452  itunitc  10461  domtriomlem  10482  axdc3lem2  10491  zorn2lem7  10542  zornn0g  10545  pwfseqlem4a  10701  pwfseqlem4  10702  wunfi  10761  wunex2  10778  wuncval  10782  rankcf  10817  tskuni  10823  axgroth6  10868  axgroth3  10871  axgroth4  10872  fzoss1  13726  fsuppmapnn0fiubex  14033  hashf1lem2  14495  cleq1lem  15021  rtrclreclem4  15100  sumeq1  15725  fsumcvg3  15765  fsum2d  15807  fsumabs  15837  fsumrlim  15847  fsumo1  15848  fsumiun  15857  prodeq1f  15942  prodeq1  15943  fprod2d  16017  lcmfunsnlem  16678  coprmprod  16698  vdwmc  17016  prmgaplem3  17091  prmgaplem4  17092  restsspw  17476  ismred2  17646  mrcval  17653  mrcuni  17664  acsfn  17702  isssc  17864  drsdirfi  18351  ipodrsima  18586  cntzssv  19346  pmtrfrn  19476  pmtrrn2  19478  pmtrdifellem1  19494  pmtrdifellem2  19495  sylow2alem2  19636  sylow2a  19637  efgval  19735  gsumzaddlem  19939  ablfac1eulem  20092  rgspnval  20612  lspval  20973  lspindpi  21134  znf1o  21570  zntoslem  21575  aspval  21893  mplsubglem  22019  mpllsslem  22020  mplcoe1  22055  mplcoe5  22058  mdetunilem9  22626  uniopn  22903  fiinopn  22907  fiinbas  22959  baspartn  22961  eltg2  22965  eltg3  22969  topbas  22979  pptbas  23015  clsval  23045  neiint  23112  neips  23121  opnneissb  23122  opnssneib  23123  innei  23133  neiptoptop  23139  neiptopnei  23140  restbas  23166  restcld  23180  neitr  23188  restcls  23189  restntr  23190  cnpdis  23301  cmpsublem  23407  cmpsub  23408  fiuncmp  23412  unconn  23437  1stcfb  23453  2ndc1stc  23459  1stcrest  23461  2ndcctbss  23463  2ndcomap  23466  dis2ndc  23468  lly1stc  23504  refssex  23519  refun0  23523  llycmpkgen2  23558  txbas  23575  eltx  23576  ptuni2  23584  neitx  23615  ptpjopn  23620  ptcld  23621  txlm  23656  tx1stc  23658  txkgen  23660  xkopt  23663  xkococnlem  23667  ptcmpfi  23821  fbssfi  23845  opnfbas  23850  isfil2  23864  isfildlem  23865  snfil  23872  fsubbas  23875  ssfg  23880  fgss2  23882  fgcl  23886  fbasrn  23892  fgtr  23898  ufli  23922  uffix  23929  rnelfmlem  23960  fclscf  24033  alexsublem  24052  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  tmdgsum2  24104  subgntr  24115  opnsubg  24116  qustgpopn  24128  tsmsfbas  24136  tsmsgsum  24147  tsmsres  24152  tsmsf1o  24153  tsmsxplem1  24161  tsmsxp  24163  isust  24212  ustssel  24214  ustincl  24216  ustdiag  24217  ustinvel  24218  ustexhalf  24219  ustexsym  24224  ust0  24228  restutop  24246  ustuqtop4  24253  utopsnneiplem  24256  blssexps  24436  blssex  24437  neibl  24514  blcld  24518  met1stc  24534  met2ndci  24535  metrest  24537  prdsxmslem2  24542  metustfbas  24570  cfilucfil  24572  metuel2  24578  metustbl  24579  restmetu  24583  dscopn  24586  isngp2  24610  tgioo  24817  tgqioo  24821  zdis  24838  xrge0tsms  24856  fsumcn  24894  volivth  25642  vitalilem2  25644  itgfsum  25862  limcun  25930  recnprss  25939  dvmptfsum  26013  ftc1a  26078  plyssc  26239  efopn  26700  jensen  27032  brsslt  27830  madef  27895  tglnunirn  28556  lpvtx  29085  umgredgprv  29124  usgredgprvALT  29212  issubgr2  29289  subgrprop2  29291  egrsubgr  29294  0uhgrsubgr  29296  frcond3  30288  hhsssh  31288  shintcl  31349  chintcl  31351  spanval  31352  omlsi  31423  pjoml  31455  chnlen0  31463  chsscon3  31519  chlejb1  31531  chnle  31533  spanun  31564  h1datom  31601  cmbr4i  31620  pjoml2  31630  pjoml3  31631  lecm  31636  osumcor2i  31663  osum  31664  spansncv  31672  pjcjt2  31711  pjopyth  31739  hstel2  32238  stj  32254  stcltr1i  32293  mdi  32314  mdbr3  32316  mdbr4  32317  dmdbr  32318  dmdmd  32319  dmdbr5  32327  mdsl1i  32340  mdslmd1lem3  32346  mdslmd1lem4  32347  mdslmd1i  32348  csmdsymi  32353  atss  32365  atom1d  32372  superpos  32373  chcv1  32374  shatomici  32377  shatomistici  32380  hatomistici  32381  chrelat2  32389  chirredi  32413  atcvat4i  32416  mdsymlem2  32423  mdsymlem6  32427  dmdbr6ati  32442  dmdbr7ati  32443  xrge0tsmsd  33065  gsumle  33101  gsumvsca1  33232  gsumvsca2  33233  prmidl  33468  ismxidl  33490  zarcls1  33868  zarclsun  33869  zarclsiin  33870  zarclsint  33871  zarclssn  33872  zartop  33875  zartopon  33876  zart0  33878  zarmxt1  33879  zarcmp  33881  rhmpreimacnlem  33883  rhmpreimacn  33884  tpr2rico  33911  issiga  34113  isrnsiga  34114  sigagenval  34141  measiuns  34218  dya2icoseg  34279  dya2iocnrect  34283  dya2iocuni  34285  carsgmon  34316  carsgsigalem  34317  carsgclctunlem2  34321  carsgclctun  34323  pmeasmono  34326  pmeasadd  34327  bnj517  34899  bnj1118  34998  bnj1145  35007  bnj1154  35013  bnj1452  35066  bnj1498  35075  fineqvpow  35110  fineqvac  35111  fineqvacALT  35112  pthhashvtx  35133  kur14lem1  35211  cvmopnlem  35283  dfon2lem3  35786  dfon2lem7  35790  brsset  35890  fness  36350  fneref  36351  fnessref  36358  neibastop2lem  36361  topmeet  36365  fnejoin2  36370  tailfb  36378  filnetlem4  36382  onsucsuccmpi  36444  bj-snglss  36971  bj-elpwgALT  37055  bj-restpw  37093  bj-imdirco  37191  dissneqlem  37341  relowlssretop  37364  relowlpssretop  37365  ctbssinf  37407  pibt2  37418  matunitlindflem1  37623  ptrecube  37627  poimirlem29  37656  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  indexa  37740  indexdom  37741  neificl  37760  istotbnd3  37778  sstotbnd2  37781  sstotbnd  37782  equivtotbnd  37785  ssbnd  37795  heiborlem1  37818  heiborlem6  37823  heiborlem8  37825  heiborlem10  37827  unichnidl  38038  pridl  38044  ismaxidl  38047  igenval  38068  igenval2  38073  ispridlc  38077  relcnveq3  38322  iss2  38345  elrelscnveq3  38492  brssr  38502  lsmsat  39009  lssatomic  39012  lssats  39013  lsat0cv  39034  lcvexchlem4  39038  lcvexchlem5  39039  lsatcvatlem  39050  l1cvpat  39055  ispsubsp  39747  linepsubN  39754  pclvalN  39892  ispsubclN  39939  ispsubcl2N  39949  pclfinclN  39952  diaelrnN  41047  docavalN  41125  dochval  41353  dvh4dimat  41440  dochexmidlem1  41462  lpolconN  41489  mapdordlem2  41639  eqresfnbd  42273  ismrcd1  42709  ismrcd2  42710  ismrc  42712  mzpcompact2lem  42762  aomclem6  43071  hbtlem6  43141  onintunirab  43239  rp-brsslt  43436  ssficl  43582  ssuncl  43583  ssdifcl  43584  sssymdifcl  43585  elmapintrab  43589  clcnvlem  43636  iunrelexpmin1  43721  iunrelexpmin2  43725  clsk3nimkb  44053  clsk1indlem1  44058  isotone1  44061  isotone2  44062  ntrclsiso  44080  gneispace  44147  gneispacess2  44159  onfrALTlem5  44562  onfrALTlem5VD  44905  relpfrlem  44974  modelaxreplem1  44995  islptre  45634  dvmptconst  45930  dvmptidg  45932  dvmulcncf  45940  dvdivcncf  45942  dvmptfprod  45960  stoweidlem51  46066  stoweidlem52  46067  fourierdlem103  46224  fourierdlem104  46225  ioorrnopnlem  46319  ioorrnopnxrlem  46321  salgenval  46336  ovnval2  46560  ovncvrrp  46579  ovnsubaddlem1  46585  ovnsubadd  46587  ovncvr2  46626  hspmbl  46644  elsetpreimafvssdm  47373  isubgredg  47852  uhgrimisgrgriclem  47898  grimedg  47903  grtrissvtx  47911  grtrimap  47915  stgredgiun  47925  isubgr3stgrlem6  47938  isubgr3stgrlem7  47939  uspgrlimlem1  47955  uspgrlimlem2  47956  uspgrlimlem3  47957  uspgrlimlem4  47958  grlimgrtrilem1  47961  grlimgrtrilem2  47962  grlimgrtri  47963  usgrexmpl1lem  47980  usgrexmpl2lem  47985  uspgrsprfo  48064  unilbss  48737  sepfsepc  48825  unilbeu  48874  ipolubdm  48876  ipoglbdm  48879  setrec1lem1  49206  setrec1lem4  49209  setrec2fun  49211  elsetrecslem  49218  elpglem2  49231