Theorem sseq1 3984

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

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 2707

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

This theorem is referenced by:  sseq12  3986  sseq1i  3987  sseq1d  3990  nssne2  4022  psseq1  4065  uneqdifeq  4468  sbss  4494  pwjust  4576  elpwg  4578  pwpw0  4789  sssn  4802  ssunsn2  4803  unimax  4920  trss  5240  al0ssb  5278  sseliALT  5279  elssabg  5313  intabs  5319  vpwex  5347  nnullss  5437  exss  5438  friOLD  5612  releq  5755  iss  6022  relcnvtrg  6255  fununi  6610  ssimaex  6963  isofrlem  7332  onssmin  7784  tfis  7848  tfisi  7852  funcnvuni  7926  ffoss  7942  f1oweALT  7969  frxp  8123  frxp2  8141  frrlem1  8283  frrlem13  8295  wfrlem1OLD  8320  wfrlem4OLD  8324  wfrlem15OLD  8335  tfrlem1  8388  oawordeu  8565  coflton  8681  cofon1  8682  cofon2  8683  naddunif  8703  qsss  8790  boxcutc  8953  sbthlem2  9096  sbth  9105  findcard2d  9178  ssfi  9185  sbthfi  9211  php  9219  phpOLD  9229  isinf  9266  isinfOLD  9267  unbnn2  9303  domunfican  9331  fiint  9336  fiintOLD  9337  finsschain  9369  indexfi  9370  dffi3  9441  hartogslem1  9554  cantnfval2  9681  cantnfle  9683  cantnflem1  9701  tz9.1  9741  setind  9746  tcvalg  9750  frmin  9761  scott0  9898  bnd2  9905  carduni  9993  cardaleph  10101  alephinit  10107  aceq3lem  10132  dfac12lem3  10158  infmap2  10229  cflem  10257  cflemOLD  10258  cflm  10262  cflecard  10265  cfeq0  10268  cfsuc  10269  cfflb  10271  cfslb  10278  cfslb2n  10280  coftr  10285  fin23lem13  10344  fin23lem16  10347  fin23lem19  10348  fin23lem29  10353  fin1a2lem13  10424  itunitc  10433  domtriomlem  10454  axdc3lem2  10463  zorn2lem7  10514  zornn0g  10517  pwfseqlem4a  10673  pwfseqlem4  10674  wunfi  10733  wunex2  10750  wuncval  10754  rankcf  10789  tskuni  10795  axgroth6  10840  axgroth3  10843  axgroth4  10844  fzoss1  13701  fsuppmapnn0fiubex  14008  hashf1lem2  14472  cleq1lem  14999  rtrclreclem4  15078  sumeq1  15703  fsumcvg3  15743  fsum2d  15785  fsumabs  15815  fsumrlim  15825  fsumo1  15826  fsumiun  15835  prodeq1f  15920  prodeq1  15921  fprod2d  15995  lcmfunsnlem  16658  coprmprod  16678  vdwmc  16996  prmgaplem3  17071  prmgaplem4  17072  restsspw  17443  ismred2  17613  mrcval  17620  mrcuni  17631  acsfn  17669  isssc  17831  drsdirfi  18315  ipodrsima  18549  cntzssv  19309  pmtrfrn  19437  pmtrrn2  19439  pmtrdifellem1  19455  pmtrdifellem2  19456  sylow2alem2  19597  sylow2a  19598  efgval  19696  gsumzaddlem  19900  ablfac1eulem  20053  rgspnval  20570  lspval  20930  lspindpi  21091  znf1o  21510  zntoslem  21515  aspval  21831  mplsubglem  21957  mpllsslem  21958  mplcoe1  21993  mplcoe5  21996  mdetunilem9  22556  uniopn  22833  fiinopn  22837  fiinbas  22888  baspartn  22890  eltg2  22894  eltg3  22898  topbas  22908  pptbas  22944  clsval  22973  neiint  23040  neips  23049  opnneissb  23050  opnssneib  23051  innei  23061  neiptoptop  23067  neiptopnei  23068  restbas  23094  restcld  23108  neitr  23116  restcls  23117  restntr  23118  cnpdis  23229  cmpsublem  23335  cmpsub  23336  fiuncmp  23340  unconn  23365  1stcfb  23381  2ndc1stc  23387  1stcrest  23389  2ndcctbss  23391  2ndcomap  23394  dis2ndc  23396  lly1stc  23432  refssex  23447  refun0  23451  llycmpkgen2  23486  txbas  23503  eltx  23504  ptuni2  23512  neitx  23543  ptpjopn  23548  ptcld  23549  txlm  23584  tx1stc  23586  txkgen  23588  xkopt  23591  xkococnlem  23595  ptcmpfi  23749  fbssfi  23773  opnfbas  23778  isfil2  23792  isfildlem  23793  snfil  23800  fsubbas  23803  ssfg  23808  fgss2  23810  fgcl  23814  fbasrn  23820  fgtr  23826  ufli  23850  uffix  23857  rnelfmlem  23888  fclscf  23961  alexsublem  23980  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALTlem4  23986  alexsubALT  23987  tmdgsum2  24032  subgntr  24043  opnsubg  24044  qustgpopn  24056  tsmsfbas  24064  tsmsgsum  24075  tsmsres  24080  tsmsf1o  24081  tsmsxplem1  24089  tsmsxp  24091  isust  24140  ustssel  24142  ustincl  24144  ustdiag  24145  ustinvel  24146  ustexhalf  24147  ustexsym  24152  ust0  24156  restutop  24174  ustuqtop4  24181  utopsnneiplem  24184  blssexps  24363  blssex  24364  neibl  24438  blcld  24442  met1stc  24458  met2ndci  24459  metrest  24461  prdsxmslem2  24466  metustfbas  24494  cfilucfil  24496  metuel2  24502  metustbl  24503  restmetu  24507  dscopn  24510  isngp2  24534  tgioo  24733  tgqioo  24737  zdis  24754  xrge0tsms  24772  fsumcn  24810  volivth  25558  vitalilem2  25560  itgfsum  25778  limcun  25846  recnprss  25855  dvmptfsum  25929  ftc1a  25994  plyssc  26155  efopn  26617  jensen  26949  brsslt  27747  madef  27812  tglnunirn  28473  lpvtx  28993  umgredgprv  29032  usgredgprvALT  29120  issubgr2  29197  subgrprop2  29199  egrsubgr  29202  0uhgrsubgr  29204  frcond3  30196  hhsssh  31196  shintcl  31257  chintcl  31259  spanval  31260  omlsi  31331  pjoml  31363  chnlen0  31371  chsscon3  31427  chlejb1  31439  chnle  31441  spanun  31472  h1datom  31509  cmbr4i  31528  pjoml2  31538  pjoml3  31539  lecm  31544  osumcor2i  31571  osum  31572  spansncv  31580  pjcjt2  31619  pjopyth  31647  hstel2  32146  stj  32162  stcltr1i  32201  mdi  32222  mdbr3  32224  mdbr4  32225  dmdbr  32226  dmdmd  32227  dmdbr5  32235  mdsl1i  32248  mdslmd1lem3  32254  mdslmd1lem4  32255  mdslmd1i  32256  csmdsymi  32261  atss  32273  atom1d  32280  superpos  32281  chcv1  32282  shatomici  32285  shatomistici  32288  hatomistici  32289  chrelat2  32297  chirredi  32321  atcvat4i  32324  mdsymlem2  32331  mdsymlem6  32335  dmdbr6ati  32350  dmdbr7ati  32351  xrge0tsmsd  33002  gsumle  33038  gsumvsca1  33169  gsumvsca2  33170  prmidl  33401  ismxidl  33423  constrfiss  33731  zarcls1  33846  zarclsun  33847  zarclsiin  33848  zarclsint  33849  zarclssn  33850  zartop  33853  zartopon  33854  zart0  33856  zarmxt1  33857  zarcmp  33859  rhmpreimacnlem  33861  rhmpreimacn  33862  tpr2rico  33889  issiga  34089  isrnsiga  34090  sigagenval  34117  measiuns  34194  dya2icoseg  34255  dya2iocnrect  34259  dya2iocuni  34261  carsgmon  34292  carsgsigalem  34293  carsgclctunlem2  34297  carsgclctun  34299  pmeasmono  34302  pmeasadd  34303  bnj517  34862  bnj1118  34961  bnj1145  34970  bnj1154  34976  bnj1452  35029  bnj1498  35038  fineqvpow  35073  fineqvac  35074  fineqvacALT  35075  pthhashvtx  35096  kur14lem1  35174  cvmopnlem  35246  dfon2lem3  35749  dfon2lem7  35753  brsset  35853  fness  36313  fneref  36314  fnessref  36321  neibastop2lem  36324  topmeet  36328  fnejoin2  36333  tailfb  36341  filnetlem4  36345  onsucsuccmpi  36407  bj-snglss  36934  bj-elpwgALT  37018  bj-restpw  37056  bj-imdirco  37154  dissneqlem  37304  relowlssretop  37327  relowlpssretop  37328  ctbssinf  37370  pibt2  37381  matunitlindflem1  37586  ptrecube  37590  poimirlem29  37619  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  indexa  37703  indexdom  37704  neificl  37723  istotbnd3  37741  sstotbnd2  37744  sstotbnd  37745  equivtotbnd  37748  ssbnd  37758  heiborlem1  37781  heiborlem6  37786  heiborlem8  37788  heiborlem10  37790  unichnidl  38001  pridl  38007  ismaxidl  38010  igenval  38031  igenval2  38036  ispridlc  38040  relcnveq3  38285  iss2  38308  elrelscnveq3  38455  brssr  38465  lsmsat  38972  lssatomic  38975  lssats  38976  lsat0cv  38997  lcvexchlem4  39001  lcvexchlem5  39002  lsatcvatlem  39013  l1cvpat  39018  ispsubsp  39710  linepsubN  39717  pclvalN  39855  ispsubclN  39902  ispsubcl2N  39912  pclfinclN  39915  diaelrnN  41010  docavalN  41088  dochval  41316  dvh4dimat  41403  dochexmidlem1  41425  lpolconN  41452  mapdordlem2  41602  eqresfnbd  42230  ismrcd1  42668  ismrcd2  42669  ismrc  42671  mzpcompact2lem  42721  aomclem6  43030  hbtlem6  43100  onintunirab  43198  rp-brsslt  43394  ssficl  43540  ssuncl  43541  ssdifcl  43542  sssymdifcl  43543  elmapintrab  43547  clcnvlem  43594  iunrelexpmin1  43679  iunrelexpmin2  43683  clsk3nimkb  44011  clsk1indlem1  44016  isotone1  44019  isotone2  44020  ntrclsiso  44038  gneispace  44105  gneispacess2  44117  onfrALTlem5  44515  onfrALTlem5VD  44857  relpfrlem  44926  modelaxreplem1  44951  islptre  45596  dvmptconst  45892  dvmptidg  45894  dvmulcncf  45902  dvdivcncf  45904  dvmptfprod  45922  stoweidlem51  46028  stoweidlem52  46029  fourierdlem103  46186  fourierdlem104  46187  ioorrnopnlem  46281  ioorrnopnxrlem  46283  salgenval  46298  ovnval2  46522  ovncvrrp  46541  ovnsubaddlem1  46547  ovnsubadd  46549  ovncvr2  46588  hspmbl  46606  elsetpreimafvssdm  47348  isubgredg  47827  uhgrimisgrgriclem  47891  grimedg  47896  grtrissvtx  47904  grtrimap  47908  stgredgiun  47918  isubgr3stgrlem6  47931  isubgr3stgrlem7  47932  uspgrlimlem1  47948  uspgrlimlem2  47949  uspgrlimlem3  47950  uspgrlimlem4  47951  grlimgrtrilem1  47954  grlimgrtrilem2  47955  grlimgrtri  47956  usgrexmpl1lem  47973  usgrexmpl2lem  47978  uspgrsprfo  48071  unilbss  48744  sepfsepc  48850  unilbeu  48907  ipolubdm  48909  ipoglbdm  48912  discsubc  48979  iinfconstbas  48981  setrec1lem1  49499  setrec1lem4  49502  setrec2fun  49504  elsetrecslem  49511  elpglem2  49524