Theorem sseq1 3947

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

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 2708

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

This theorem is referenced by:  sseq12  3949  sseq1i  3950  sseq1d  3953  nssne2  3985  psseq1  4030  uneqdifeq  4432  sbss  4460  pwjust  4542  elpwg  4544  pwpw0  4756  sssn  4769  ssunsn2  4770  unimax  4887  trss  5202  al0ssb  5243  sseliALT  5244  elssabg  5284  intabs  5290  vpwex  5319  nnullss  5414  exss  5415  releq  5733  iss  6000  relcnvtrg  6231  fununi  6573  ssimaex  6925  isofrlem  7295  onssmin  7746  tfis  7806  tfisi  7810  funcnvuni  7883  ffoss  7899  f1oweALT  7925  frxp  8076  frxp2  8094  frrlem1  8236  frrlem13  8248  tfrlem1  8315  oawordeu  8490  coflton  8607  cofon1  8608  cofon2  8609  naddunif  8629  qsss  8722  boxcutc  8889  sbthlem2  9026  sbth  9035  findcard2d  9101  ssfi  9107  sbthfi  9133  php  9141  isinf  9175  unbnn2  9207  domunfican  9232  fiint  9237  finsschain  9269  indexfi  9270  dffi3  9344  hartogslem1  9457  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  13641  fsuppmapnn0fiubex  13954  hashf1lem2  14418  cleq1lem  14944  rtrclreclem4  15023  sumeq1  15651  fsumcvg3  15691  fsum2d  15733  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  prodeq1f  15871  prodeq1  15872  fprod2d  15946  lcmfunsnlem  16610  coprmprod  16630  vdwmc  16949  prmgaplem3  17024  prmgaplem4  17025  restsspw  17394  ismred2  17565  mrcval  17576  mrcuni  17587  acsfn  17625  isssc  17787  drsdirfi  18271  ipodrsima  18507  cntzssv  19303  pmtrfrn  19433  pmtrrn2  19435  pmtrdifellem1  19451  pmtrdifellem2  19452  sylow2alem2  19593  sylow2a  19594  efgval  19692  gsumzaddlem  19896  ablfac1eulem  20049  gsumle  20120  rgspnval  20589  lspval  20970  lspindpi  21130  znf1o  21531  zntoslem  21536  aspval  21852  mplsubglem  21977  mpllsslem  21978  mplcoe1  22015  mplcoe5  22018  mdetunilem9  22585  uniopn  22862  fiinopn  22866  fiinbas  22917  baspartn  22919  eltg2  22923  eltg3  22927  topbas  22937  pptbas  22973  clsval  23002  neiint  23069  neips  23078  opnneissb  23079  opnssneib  23080  innei  23090  neiptoptop  23096  neiptopnei  23097  restbas  23123  restcld  23137  neitr  23145  restcls  23146  restntr  23147  cnpdis  23258  cmpsublem  23364  cmpsub  23365  fiuncmp  23369  unconn  23394  1stcfb  23410  2ndc1stc  23416  1stcrest  23418  2ndcctbss  23420  2ndcomap  23423  dis2ndc  23425  lly1stc  23461  refssex  23476  refun0  23480  llycmpkgen2  23515  txbas  23532  eltx  23533  ptuni2  23541  neitx  23572  ptpjopn  23577  ptcld  23578  txlm  23613  tx1stc  23615  txkgen  23617  xkopt  23620  xkococnlem  23624  ptcmpfi  23778  fbssfi  23802  opnfbas  23807  isfil2  23821  isfildlem  23822  snfil  23829  fsubbas  23832  ssfg  23837  fgss2  23839  fgcl  23843  fbasrn  23849  fgtr  23855  ufli  23879  uffix  23886  rnelfmlem  23917  fclscf  23990  alexsublem  24009  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  tmdgsum2  24061  subgntr  24072  opnsubg  24073  qustgpopn  24085  tsmsfbas  24093  tsmsgsum  24104  tsmsres  24109  tsmsf1o  24110  tsmsxplem1  24118  tsmsxp  24120  isust  24169  ustssel  24171  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  ustexsym  24181  ust0  24185  restutop  24202  ustuqtop4  24209  utopsnneiplem  24212  blssexps  24391  blssex  24392  neibl  24466  blcld  24470  met1stc  24486  met2ndci  24487  metrest  24489  prdsxmslem2  24494  metustfbas  24522  cfilucfil  24524  metuel2  24530  metustbl  24531  restmetu  24535  dscopn  24538  isngp2  24562  tgioo  24761  tgqioo  24765  zdis  24782  xrge0tsms  24800  fsumcn  24837  volivth  25574  vitalilem2  25576  itgfsum  25794  limcun  25862  recnprss  25871  dvmptfsum  25942  ftc1a  26004  plyssc  26165  efopn  26622  jensen  26952  brslts  27754  madef  27828  tglnunirn  28616  lpvtx  29137  umgredgprv  29176  usgredgprvALT  29264  issubgr2  29341  subgrprop2  29343  egrsubgr  29346  0uhgrsubgr  29348  frcond3  30339  hhsssh  31340  shintcl  31401  chintcl  31403  spanval  31404  omlsi  31475  pjoml  31507  chnlen0  31515  chsscon3  31571  chlejb1  31583  chnle  31585  spanun  31616  h1datom  31653  cmbr4i  31672  pjoml2  31682  pjoml3  31683  lecm  31688  osumcor2i  31715  osum  31716  spansncv  31724  pjcjt2  31763  pjopyth  31791  hstel2  32290  stj  32306  stcltr1i  32345  mdi  32366  mdbr3  32368  mdbr4  32369  dmdbr  32370  dmdmd  32371  dmdbr5  32379  mdsl1i  32392  mdslmd1lem3  32398  mdslmd1lem4  32399  mdslmd1i  32400  csmdsymi  32405  atss  32417  atom1d  32424  superpos  32425  chcv1  32426  shatomici  32429  shatomistici  32432  hatomistici  32433  chrelat2  32441  chirredi  32465  atcvat4i  32468  mdsymlem2  32475  mdsymlem6  32479  dmdbr6ati  32494  dmdbr7ati  32495  xrge0tsmsd  33134  gsumvsca1  33287  gsumvsca2  33288  prmidl  33500  ismxidl  33522  constrfiss  33895  zarcls1  34013  zarclsun  34014  zarclsiin  34015  zarclsint  34016  zarclssn  34017  zartop  34020  zartopon  34021  zart0  34023  zarmxt1  34024  zarcmp  34026  rhmpreimacnlem  34028  rhmpreimacn  34029  tpr2rico  34056  issiga  34256  isrnsiga  34257  sigagenval  34284  measiuns  34361  dya2icoseg  34421  dya2iocnrect  34425  dya2iocuni  34427  carsgmon  34458  carsgsigalem  34459  carsgclctunlem2  34463  carsgclctun  34465  pmeasmono  34468  pmeasadd  34469  bnj517  35027  bnj1118  35126  bnj1145  35135  bnj1154  35141  bnj1452  35194  bnj1498  35203  fineqvpow  35259  fineqvac  35260  fineqvacALT  35261  setindregs  35274  tz9.1regs  35278  fineqvr1ombregs  35282  vonf1owev  35290  pthhashvtx  35310  kur14lem1  35388  cvmopnlem  35460  dfon2lem3  35965  dfon2lem7  35969  brsset  36069  fness  36531  fneref  36532  fnessref  36539  neibastop2lem  36542  topmeet  36546  fnejoin2  36551  tailfb  36559  filnetlem4  36563  onsucsuccmpi  36625  ttcwf2  36707  ttcexg  36714  bj-snglss  37277  bj-elpwgALT  37361  bj-restpw  37404  bj-imdirco  37504  dissneqlem  37656  relowlssretop  37679  relowlpssretop  37680  ctbssinf  37722  pibt2  37733  matunitlindflem1  37937  ptrecube  37941  poimirlem29  37970  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  indexa  38054  indexdom  38055  neificl  38074  istotbnd3  38092  sstotbnd2  38095  sstotbnd  38096  equivtotbnd  38099  ssbnd  38109  heiborlem1  38132  heiborlem6  38137  heiborlem8  38139  heiborlem10  38141  unichnidl  38352  pridl  38358  ismaxidl  38361  igenval  38382  igenval2  38387  ispridlc  38391  relcnveq3  38648  iss2  38665  brssr  38902  elrelscnveq3  38948  lsmsat  39454  lssatomic  39457  lssats  39458  lsat0cv  39479  lcvexchlem4  39483  lcvexchlem5  39484  lsatcvatlem  39495  l1cvpat  39500  ispsubsp  40191  linepsubN  40198  pclvalN  40336  ispsubclN  40383  ispsubcl2N  40393  pclfinclN  40396  diaelrnN  41491  docavalN  41569  dochval  41797  dvh4dimat  41884  dochexmidlem1  41906  lpolconN  41933  mapdordlem2  42083  eqresfnbd  42673  ismrcd1  43130  ismrcd2  43131  ismrc  43133  mzpcompact2lem  43183  aomclem6  43487  hbtlem6  43557  onintunirab  43655  rp-brsslt  43850  ssficl  43996  ssuncl  43997  ssdifcl  43998  sssymdifcl  43999  elmapintrab  44003  clcnvlem  44050  iunrelexpmin1  44135  iunrelexpmin2  44139  clsk3nimkb  44467  clsk1indlem1  44472  isotone1  44475  isotone2  44476  ntrclsiso  44494  gneispace  44561  gneispacess2  44573  onfrALTlem5  44969  onfrALTlem5VD  45311  relpfrlem  45380  modelaxreplem1  45405  islptre  46049  dvmptconst  46343  dvmptidg  46345  dvmulcncf  46353  dvdivcncf  46355  dvmptfprod  46373  stoweidlem51  46479  stoweidlem52  46480  fourierdlem103  46637  fourierdlem104  46638  ioorrnopnlem  46732  ioorrnopnxrlem  46734  salgenval  46749  ovnval2  46973  ovncvrrp  46992  ovnsubaddlem1  46998  ovnsubadd  47000  ovncvr2  47039  hspmbl  47057  elsetpreimafvssdm  47846  isubgredg  48342  uhgrimisgrgriclem  48406  grimedg  48411  grtrissvtx  48420  grtrimap  48424  stgredgiun  48434  isubgr3stgrlem6  48447  isubgr3stgrlem7  48448  uspgrlimlem1  48464  uspgrlimlem2  48465  uspgrlimlem3  48466  uspgrlimlem4  48467  clnbgrvtxedg  48470  grlimedgclnbgr  48471  grlimpredg  48474  grlimprclnbgrvtx  48475  grlimgredgex  48476  grlimgrtrilem1  48477  grlimgrtrilem2  48478  grlimgrtri  48479  usgrexmpl1lem  48497  usgrexmpl2lem  48502  uspgrsprfo  48624  unilbss  49293  sepfsepc  49403  unilbeu  49460  ipolubdm  49462  ipoglbdm  49465  discsubc  49539  iinfconstbas  49541  setrec1lem1  50162  setrec1lem4  50165  setrec2fun  50167  elsetrecslem  50174  elpglem2  50187