Theorem sseq1 3957

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 3947	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3938	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3938	. . . 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 1541   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3916

This theorem is referenced by:  sseq12  3959  sseq1i  3960  sseq1d  3963  nssne2  3995  psseq1  4041  uneqdifeq  4444  sbss  4470  pwjust  4552  elpwg  4554  pwpw0  4766  sssn  4779  ssunsn2  4780  unimax  4897  trss  5212  al0ssb  5250  sseliALT  5251  elssabg  5285  intabs  5291  vpwex  5319  nnullss  5407  exss  5408  releq  5723  iss  5991  relcnvtrg  6222  fununi  6564  ssimaex  6916  isofrlem  7283  onssmin  7734  tfis  7794  tfisi  7798  funcnvuni  7871  ffoss  7887  f1oweALT  7913  frxp  8065  frxp2  8083  frrlem1  8225  frrlem13  8237  tfrlem1  8304  oawordeu  8479  coflton  8595  cofon1  8596  cofon2  8597  naddunif  8617  qsss  8709  boxcutc  8874  sbthlem2  9011  sbth  9020  findcard2d  9086  ssfi  9092  sbthfi  9118  php  9126  isinf  9159  unbnn2  9191  domunfican  9216  fiint  9221  finsschain  9253  indexfi  9254  dffi3  9325  hartogslem1  9438  cantnfval2  9569  cantnfle  9571  cantnflem1  9589  tz9.1  9629  tcvalg  9636  setind  9647  frmin  9652  scott0  9789  bnd2  9796  carduni  9884  cardaleph  9990  alephinit  9996  aceq3lem  10021  dfac12lem3  10047  infmap2  10118  cflem  10146  cflemOLD  10147  cflm  10151  cflecard  10154  cfeq0  10157  cfsuc  10158  cfflb  10160  cfslb  10167  cfslb2n  10169  coftr  10174  fin23lem13  10233  fin23lem16  10236  fin23lem19  10237  fin23lem29  10242  fin1a2lem13  10313  itunitc  10322  domtriomlem  10343  axdc3lem2  10352  zorn2lem7  10403  zornn0g  10406  pwfseqlem4a  10562  pwfseqlem4  10563  wunfi  10622  wunex2  10639  wuncval  10643  rankcf  10678  tskuni  10684  axgroth6  10729  axgroth3  10732  axgroth4  10733  fzoss1  13596  fsuppmapnn0fiubex  13909  hashf1lem2  14373  cleq1lem  14899  rtrclreclem4  14978  sumeq1  15606  fsumcvg3  15646  fsum2d  15688  fsumabs  15718  fsumrlim  15728  fsumo1  15729  fsumiun  15738  prodeq1f  15823  prodeq1  15824  fprod2d  15898  lcmfunsnlem  16562  coprmprod  16582  vdwmc  16900  prmgaplem3  16975  prmgaplem4  16976  restsspw  17345  ismred2  17515  mrcval  17526  mrcuni  17537  acsfn  17575  isssc  17737  drsdirfi  18221  ipodrsima  18457  cntzssv  19250  pmtrfrn  19380  pmtrrn2  19382  pmtrdifellem1  19398  pmtrdifellem2  19399  sylow2alem2  19540  sylow2a  19541  efgval  19639  gsumzaddlem  19843  ablfac1eulem  19996  gsumle  20067  rgspnval  20537  lspval  20918  lspindpi  21079  znf1o  21498  zntoslem  21503  aspval  21820  mplsubglem  21946  mpllsslem  21947  mplcoe1  21982  mplcoe5  21985  mdetunilem9  22545  uniopn  22822  fiinopn  22826  fiinbas  22877  baspartn  22879  eltg2  22883  eltg3  22887  topbas  22897  pptbas  22933  clsval  22962  neiint  23029  neips  23038  opnneissb  23039  opnssneib  23040  innei  23050  neiptoptop  23056  neiptopnei  23057  restbas  23083  restcld  23097  neitr  23105  restcls  23106  restntr  23107  cnpdis  23218  cmpsublem  23324  cmpsub  23325  fiuncmp  23329  unconn  23354  1stcfb  23370  2ndc1stc  23376  1stcrest  23378  2ndcctbss  23380  2ndcomap  23383  dis2ndc  23385  lly1stc  23421  refssex  23436  refun0  23440  llycmpkgen2  23475  txbas  23492  eltx  23493  ptuni2  23501  neitx  23532  ptpjopn  23537  ptcld  23538  txlm  23573  tx1stc  23575  txkgen  23577  xkopt  23580  xkococnlem  23584  ptcmpfi  23738  fbssfi  23762  opnfbas  23767  isfil2  23781  isfildlem  23782  snfil  23789  fsubbas  23792  ssfg  23797  fgss2  23799  fgcl  23803  fbasrn  23809  fgtr  23815  ufli  23839  uffix  23846  rnelfmlem  23877  fclscf  23950  alexsublem  23969  alexsubALTlem2  23973  alexsubALTlem3  23974  alexsubALTlem4  23975  alexsubALT  23976  tmdgsum2  24021  subgntr  24032  opnsubg  24033  qustgpopn  24045  tsmsfbas  24053  tsmsgsum  24064  tsmsres  24069  tsmsf1o  24070  tsmsxplem1  24078  tsmsxp  24080  isust  24129  ustssel  24131  ustincl  24133  ustdiag  24134  ustinvel  24135  ustexhalf  24136  ustexsym  24141  ust0  24145  restutop  24162  ustuqtop4  24169  utopsnneiplem  24172  blssexps  24351  blssex  24352  neibl  24426  blcld  24430  met1stc  24446  met2ndci  24447  metrest  24449  prdsxmslem2  24454  metustfbas  24482  cfilucfil  24484  metuel2  24490  metustbl  24491  restmetu  24495  dscopn  24498  isngp2  24522  tgioo  24721  tgqioo  24725  zdis  24742  xrge0tsms  24760  fsumcn  24798  volivth  25545  vitalilem2  25547  itgfsum  25765  limcun  25833  recnprss  25842  dvmptfsum  25916  ftc1a  25981  plyssc  26142  efopn  26604  jensen  26936  brsslt  27735  madef  27807  tglnunirn  28536  lpvtx  29057  umgredgprv  29096  usgredgprvALT  29184  issubgr2  29261  subgrprop2  29263  egrsubgr  29266  0uhgrsubgr  29268  frcond3  30260  hhsssh  31260  shintcl  31321  chintcl  31323  spanval  31324  omlsi  31395  pjoml  31427  chnlen0  31435  chsscon3  31491  chlejb1  31503  chnle  31505  spanun  31536  h1datom  31573  cmbr4i  31592  pjoml2  31602  pjoml3  31603  lecm  31608  osumcor2i  31635  osum  31636  spansncv  31644  pjcjt2  31683  pjopyth  31711  hstel2  32210  stj  32226  stcltr1i  32265  mdi  32286  mdbr3  32288  mdbr4  32289  dmdbr  32290  dmdmd  32291  dmdbr5  32299  mdsl1i  32312  mdslmd1lem3  32318  mdslmd1lem4  32319  mdslmd1i  32320  csmdsymi  32325  atss  32337  atom1d  32344  superpos  32345  chcv1  32346  shatomici  32349  shatomistici  32352  hatomistici  32353  chrelat2  32361  chirredi  32385  atcvat4i  32388  mdsymlem2  32395  mdsymlem6  32399  dmdbr6ati  32414  dmdbr7ati  32415  xrge0tsmsd  33053  gsumvsca1  33206  gsumvsca2  33207  prmidl  33416  ismxidl  33438  constrfiss  33775  zarcls1  33893  zarclsun  33894  zarclsiin  33895  zarclsint  33896  zarclssn  33897  zartop  33900  zartopon  33901  zart0  33903  zarmxt1  33904  zarcmp  33906  rhmpreimacnlem  33908  rhmpreimacn  33909  tpr2rico  33936  issiga  34136  isrnsiga  34137  sigagenval  34164  measiuns  34241  dya2icoseg  34301  dya2iocnrect  34305  dya2iocuni  34307  carsgmon  34338  carsgsigalem  34339  carsgclctunlem2  34343  carsgclctun  34345  pmeasmono  34348  pmeasadd  34349  bnj517  34908  bnj1118  35007  bnj1145  35016  bnj1154  35022  bnj1452  35075  bnj1498  35084  setindregs  35139  tz9.1regs  35141  fineqvr1ombregs  35146  fineqvpow  35149  fineqvac  35150  fineqvacALT  35151  vonf1owev  35163  pthhashvtx  35183  kur14lem1  35261  cvmopnlem  35333  dfon2lem3  35838  dfon2lem7  35842  brsset  35942  fness  36404  fneref  36405  fnessref  36412  neibastop2lem  36415  topmeet  36419  fnejoin2  36424  tailfb  36432  filnetlem4  36436  onsucsuccmpi  36498  bj-snglss  37025  bj-elpwgALT  37109  bj-restpw  37147  bj-imdirco  37245  dissneqlem  37395  relowlssretop  37418  relowlpssretop  37419  ctbssinf  37461  pibt2  37472  matunitlindflem1  37666  ptrecube  37670  poimirlem29  37699  mblfinlem2  37708  mblfinlem3  37709  mblfinlem4  37710  ismblfin  37711  ovoliunnfl  37712  voliunnfl  37714  volsupnfl  37715  indexa  37783  indexdom  37784  neificl  37803  istotbnd3  37821  sstotbnd2  37824  sstotbnd  37825  equivtotbnd  37828  ssbnd  37838  heiborlem1  37861  heiborlem6  37866  heiborlem8  37868  heiborlem10  37870  unichnidl  38081  pridl  38087  ismaxidl  38090  igenval  38111  igenval2  38116  ispridlc  38120  relcnveq3  38369  iss2  38386  brssr  38603  elrelscnveq3  38649  lsmsat  39117  lssatomic  39120  lssats  39121  lsat0cv  39142  lcvexchlem4  39146  lcvexchlem5  39147  lsatcvatlem  39158  l1cvpat  39163  ispsubsp  39854  linepsubN  39861  pclvalN  39999  ispsubclN  40046  ispsubcl2N  40056  pclfinclN  40059  diaelrnN  41154  docavalN  41232  dochval  41460  dvh4dimat  41547  dochexmidlem1  41569  lpolconN  41596  mapdordlem2  41746  eqresfnbd  42340  ismrcd1  42805  ismrcd2  42806  ismrc  42808  mzpcompact2lem  42858  aomclem6  43166  hbtlem6  43236  onintunirab  43334  rp-brsslt  43530  ssficl  43676  ssuncl  43677  ssdifcl  43678  sssymdifcl  43679  elmapintrab  43683  clcnvlem  43730  iunrelexpmin1  43815  iunrelexpmin2  43819  clsk3nimkb  44147  clsk1indlem1  44152  isotone1  44155  isotone2  44156  ntrclsiso  44174  gneispace  44241  gneispacess2  44253  onfrALTlem5  44649  onfrALTlem5VD  44991  relpfrlem  45060  modelaxreplem1  45085  islptre  45733  dvmptconst  46027  dvmptidg  46029  dvmulcncf  46037  dvdivcncf  46039  dvmptfprod  46057  stoweidlem51  46163  stoweidlem52  46164  fourierdlem103  46321  fourierdlem104  46322  ioorrnopnlem  46416  ioorrnopnxrlem  46418  salgenval  46433  ovnval2  46657  ovncvrrp  46676  ovnsubaddlem1  46682  ovnsubadd  46684  ovncvr2  46723  hspmbl  46741  elsetpreimafvssdm  47500  isubgredg  47980  uhgrimisgrgriclem  48044  grimedg  48049  grtrissvtx  48058  grtrimap  48062  stgredgiun  48072  isubgr3stgrlem6  48085  isubgr3stgrlem7  48086  uspgrlimlem1  48102  uspgrlimlem2  48103  uspgrlimlem3  48104  uspgrlimlem4  48105  clnbgrvtxedg  48108  grlimedgclnbgr  48109  grlimpredg  48112  grlimprclnbgrvtx  48113  grlimgredgex  48114  grlimgrtrilem1  48115  grlimgrtrilem2  48116  grlimgrtri  48117  usgrexmpl1lem  48135  usgrexmpl2lem  48140  uspgrsprfo  48262  unilbss  48932  sepfsepc  49042  unilbeu  49099  ipolubdm  49101  ipoglbdm  49104  discsubc  49179  iinfconstbas  49181  setrec1lem1  49802  setrec1lem4  49805  setrec2fun  49807  elsetrecslem  49814  elpglem2  49827