Theorem sseq1 3956

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

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 3915

This theorem is referenced by:  sseq12  3958  sseq1i  3959  sseq1d  3962  nssne2  3994  psseq1  4039  uneqdifeq  4442  sbss  4468  pwjust  4550  elpwg  4552  pwpw0  4764  sssn  4777  ssunsn2  4778  unimax  4895  trss  5210  al0ssb  5248  sseliALT  5249  elssabg  5283  intabs  5289  vpwex  5317  nnullss  5405  exss  5406  releq  5721  iss  5988  relcnvtrg  6219  fununi  6561  ssimaex  6913  isofrlem  7280  onssmin  7731  tfis  7791  tfisi  7795  funcnvuni  7868  ffoss  7884  f1oweALT  7910  frxp  8062  frxp2  8080  frrlem1  8222  frrlem13  8234  tfrlem1  8301  oawordeu  8476  coflton  8592  cofon1  8593  cofon2  8594  naddunif  8614  qsss  8706  boxcutc  8871  sbthlem2  9008  sbth  9017  findcard2d  9083  ssfi  9089  sbthfi  9115  php  9123  isinf  9156  unbnn2  9188  domunfican  9213  fiint  9218  finsschain  9250  indexfi  9251  dffi3  9322  hartogslem1  9435  cantnfval2  9566  cantnfle  9568  cantnflem1  9586  tz9.1  9626  tcvalg  9633  setind  9644  frmin  9649  scott0  9786  bnd2  9793  carduni  9881  cardaleph  9987  alephinit  9993  aceq3lem  10018  dfac12lem3  10044  infmap2  10115  cflem  10143  cflemOLD  10144  cflm  10148  cflecard  10151  cfeq0  10154  cfsuc  10155  cfflb  10157  cfslb  10164  cfslb2n  10166  coftr  10171  fin23lem13  10230  fin23lem16  10233  fin23lem19  10234  fin23lem29  10239  fin1a2lem13  10310  itunitc  10319  domtriomlem  10340  axdc3lem2  10349  zorn2lem7  10400  zornn0g  10403  pwfseqlem4a  10559  pwfseqlem4  10560  wunfi  10619  wunex2  10636  wuncval  10640  rankcf  10675  tskuni  10681  axgroth6  10726  axgroth3  10729  axgroth4  10730  fzoss1  13588  fsuppmapnn0fiubex  13901  hashf1lem2  14365  cleq1lem  14891  rtrclreclem4  14970  sumeq1  15598  fsumcvg3  15638  fsum2d  15680  fsumabs  15710  fsumrlim  15720  fsumo1  15721  fsumiun  15730  prodeq1f  15815  prodeq1  15816  fprod2d  15890  lcmfunsnlem  16554  coprmprod  16574  vdwmc  16892  prmgaplem3  16967  prmgaplem4  16968  restsspw  17337  ismred2  17507  mrcval  17518  mrcuni  17529  acsfn  17567  isssc  17729  drsdirfi  18213  ipodrsima  18449  cntzssv  19242  pmtrfrn  19372  pmtrrn2  19374  pmtrdifellem1  19390  pmtrdifellem2  19391  sylow2alem2  19532  sylow2a  19533  efgval  19631  gsumzaddlem  19835  ablfac1eulem  19988  gsumle  20059  rgspnval  20529  lspval  20910  lspindpi  21071  znf1o  21490  zntoslem  21495  aspval  21812  mplsubglem  21937  mpllsslem  21938  mplcoe1  21973  mplcoe5  21976  mdetunilem9  22536  uniopn  22813  fiinopn  22817  fiinbas  22868  baspartn  22870  eltg2  22874  eltg3  22878  topbas  22888  pptbas  22924  clsval  22953  neiint  23020  neips  23029  opnneissb  23030  opnssneib  23031  innei  23041  neiptoptop  23047  neiptopnei  23048  restbas  23074  restcld  23088  neitr  23096  restcls  23097  restntr  23098  cnpdis  23209  cmpsublem  23315  cmpsub  23316  fiuncmp  23320  unconn  23345  1stcfb  23361  2ndc1stc  23367  1stcrest  23369  2ndcctbss  23371  2ndcomap  23374  dis2ndc  23376  lly1stc  23412  refssex  23427  refun0  23431  llycmpkgen2  23466  txbas  23483  eltx  23484  ptuni2  23492  neitx  23523  ptpjopn  23528  ptcld  23529  txlm  23564  tx1stc  23566  txkgen  23568  xkopt  23571  xkococnlem  23575  ptcmpfi  23729  fbssfi  23753  opnfbas  23758  isfil2  23772  isfildlem  23773  snfil  23780  fsubbas  23783  ssfg  23788  fgss2  23790  fgcl  23794  fbasrn  23800  fgtr  23806  ufli  23830  uffix  23837  rnelfmlem  23868  fclscf  23941  alexsublem  23960  alexsubALTlem2  23964  alexsubALTlem3  23965  alexsubALTlem4  23966  alexsubALT  23967  tmdgsum2  24012  subgntr  24023  opnsubg  24024  qustgpopn  24036  tsmsfbas  24044  tsmsgsum  24055  tsmsres  24060  tsmsf1o  24061  tsmsxplem1  24069  tsmsxp  24071  isust  24120  ustssel  24122  ustincl  24124  ustdiag  24125  ustinvel  24126  ustexhalf  24127  ustexsym  24132  ust0  24136  restutop  24153  ustuqtop4  24160  utopsnneiplem  24163  blssexps  24342  blssex  24343  neibl  24417  blcld  24421  met1stc  24437  met2ndci  24438  metrest  24440  prdsxmslem2  24445  metustfbas  24473  cfilucfil  24475  metuel2  24481  metustbl  24482  restmetu  24486  dscopn  24489  isngp2  24513  tgioo  24712  tgqioo  24716  zdis  24733  xrge0tsms  24751  fsumcn  24789  volivth  25536  vitalilem2  25538  itgfsum  25756  limcun  25824  recnprss  25833  dvmptfsum  25907  ftc1a  25972  plyssc  26133  efopn  26595  jensen  26927  brsslt  27726  madef  27798  tglnunirn  28527  lpvtx  29048  umgredgprv  29087  usgredgprvALT  29175  issubgr2  29252  subgrprop2  29254  egrsubgr  29257  0uhgrsubgr  29259  frcond3  30251  hhsssh  31251  shintcl  31312  chintcl  31314  spanval  31315  omlsi  31386  pjoml  31418  chnlen0  31426  chsscon3  31482  chlejb1  31494  chnle  31496  spanun  31527  h1datom  31564  cmbr4i  31583  pjoml2  31593  pjoml3  31594  lecm  31599  osumcor2i  31626  osum  31627  spansncv  31635  pjcjt2  31674  pjopyth  31702  hstel2  32201  stj  32217  stcltr1i  32256  mdi  32277  mdbr3  32279  mdbr4  32280  dmdbr  32281  dmdmd  32282  dmdbr5  32290  mdsl1i  32303  mdslmd1lem3  32309  mdslmd1lem4  32310  mdslmd1i  32311  csmdsymi  32316  atss  32328  atom1d  32335  superpos  32336  chcv1  32337  shatomici  32340  shatomistici  32343  hatomistici  32344  chrelat2  32352  chirredi  32376  atcvat4i  32379  mdsymlem2  32386  mdsymlem6  32390  dmdbr6ati  32405  dmdbr7ati  32406  xrge0tsmsd  33049  gsumvsca1  33202  gsumvsca2  33203  prmidl  33412  ismxidl  33434  constrfiss  33785  zarcls1  33903  zarclsun  33904  zarclsiin  33905  zarclsint  33906  zarclssn  33907  zartop  33910  zartopon  33911  zart0  33913  zarmxt1  33914  zarcmp  33916  rhmpreimacnlem  33918  rhmpreimacn  33919  tpr2rico  33946  issiga  34146  isrnsiga  34147  sigagenval  34174  measiuns  34251  dya2icoseg  34311  dya2iocnrect  34315  dya2iocuni  34317  carsgmon  34348  carsgsigalem  34349  carsgclctunlem2  34353  carsgclctun  34355  pmeasmono  34358  pmeasadd  34359  bnj517  34918  bnj1118  35017  bnj1145  35026  bnj1154  35032  bnj1452  35085  bnj1498  35094  setindregs  35149  tz9.1regs  35151  fineqvr1ombregs  35156  fineqvpow  35159  fineqvac  35160  fineqvacALT  35161  vonf1owev  35173  pthhashvtx  35193  kur14lem1  35271  cvmopnlem  35343  dfon2lem3  35848  dfon2lem7  35852  brsset  35952  fness  36414  fneref  36415  fnessref  36422  neibastop2lem  36425  topmeet  36429  fnejoin2  36434  tailfb  36442  filnetlem4  36446  onsucsuccmpi  36508  bj-snglss  37035  bj-elpwgALT  37119  bj-restpw  37157  bj-imdirco  37255  dissneqlem  37405  relowlssretop  37428  relowlpssretop  37429  ctbssinf  37471  pibt2  37482  matunitlindflem1  37676  ptrecube  37680  poimirlem29  37709  mblfinlem2  37718  mblfinlem3  37719  mblfinlem4  37720  ismblfin  37721  ovoliunnfl  37722  voliunnfl  37724  volsupnfl  37725  indexa  37793  indexdom  37794  neificl  37813  istotbnd3  37831  sstotbnd2  37834  sstotbnd  37835  equivtotbnd  37838  ssbnd  37848  heiborlem1  37871  heiborlem6  37876  heiborlem8  37878  heiborlem10  37880  unichnidl  38091  pridl  38097  ismaxidl  38100  igenval  38121  igenval2  38126  ispridlc  38130  relcnveq3  38379  iss2  38396  brssr  38613  elrelscnveq3  38659  lsmsat  39127  lssatomic  39130  lssats  39131  lsat0cv  39152  lcvexchlem4  39156  lcvexchlem5  39157  lsatcvatlem  39168  l1cvpat  39173  ispsubsp  39864  linepsubN  39871  pclvalN  40009  ispsubclN  40056  ispsubcl2N  40066  pclfinclN  40069  diaelrnN  41164  docavalN  41242  dochval  41470  dvh4dimat  41557  dochexmidlem1  41579  lpolconN  41606  mapdordlem2  41756  eqresfnbd  42350  ismrcd1  42815  ismrcd2  42816  ismrc  42818  mzpcompact2lem  42868  aomclem6  43176  hbtlem6  43246  onintunirab  43344  rp-brsslt  43540  ssficl  43686  ssuncl  43687  ssdifcl  43688  sssymdifcl  43689  elmapintrab  43693  clcnvlem  43740  iunrelexpmin1  43825  iunrelexpmin2  43829  clsk3nimkb  44157  clsk1indlem1  44162  isotone1  44165  isotone2  44166  ntrclsiso  44184  gneispace  44251  gneispacess2  44263  onfrALTlem5  44659  onfrALTlem5VD  45001  relpfrlem  45070  modelaxreplem1  45095  islptre  45743  dvmptconst  46037  dvmptidg  46039  dvmulcncf  46047  dvdivcncf  46049  dvmptfprod  46067  stoweidlem51  46173  stoweidlem52  46174  fourierdlem103  46331  fourierdlem104  46332  ioorrnopnlem  46426  ioorrnopnxrlem  46428  salgenval  46443  ovnval2  46667  ovncvrrp  46686  ovnsubaddlem1  46692  ovnsubadd  46694  ovncvr2  46733  hspmbl  46751  elsetpreimafvssdm  47510  isubgredg  47990  uhgrimisgrgriclem  48054  grimedg  48059  grtrissvtx  48068  grtrimap  48072  stgredgiun  48082  isubgr3stgrlem6  48095  isubgr3stgrlem7  48096  uspgrlimlem1  48112  uspgrlimlem2  48113  uspgrlimlem3  48114  uspgrlimlem4  48115  clnbgrvtxedg  48118  grlimedgclnbgr  48119  grlimpredg  48122  grlimprclnbgrvtx  48123  grlimgredgex  48124  grlimgrtrilem1  48125  grlimgrtrilem2  48126  grlimgrtri  48127  usgrexmpl1lem  48145  usgrexmpl2lem  48150  uspgrsprfo  48272  unilbss  48942  sepfsepc  49052  unilbeu  49109  ipolubdm  49111  ipoglbdm  49114  discsubc  49189  iinfconstbas  49191  setrec1lem1  49812  setrec1lem4  49815  setrec2fun  49817  elsetrecslem  49824  elpglem2  49837