Theorem sseq1 3972

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  sseq12  3974  sseq1i  3975  sseq1d  3978  nssne2  4010  psseq1  4053  uneqdifeq  4456  sbss  4482  pwjust  4564  elpwg  4566  pwpw0  4777  sssn  4790  ssunsn2  4791  unimax  4908  trss  5225  al0ssb  5263  sseliALT  5264  elssabg  5298  intabs  5304  vpwex  5332  nnullss  5422  exss  5423  releq  5739  iss  6006  relcnvtrg  6239  fununi  6591  ssimaex  6946  isofrlem  7315  onssmin  7768  tfis  7831  tfisi  7835  funcnvuni  7908  ffoss  7924  f1oweALT  7951  frxp  8105  frxp2  8123  frrlem1  8265  frrlem13  8277  tfrlem1  8344  oawordeu  8519  coflton  8635  cofon1  8636  cofon2  8637  naddunif  8657  qsss  8749  boxcutc  8914  sbthlem2  9052  sbth  9061  findcard2d  9130  ssfi  9137  sbthfi  9163  php  9171  isinf  9207  isinfOLD  9208  unbnn2  9244  domunfican  9272  fiint  9277  fiintOLD  9278  finsschain  9310  indexfi  9311  dffi3  9382  hartogslem1  9495  cantnfval2  9622  cantnfle  9624  cantnflem1  9642  tz9.1  9682  setind  9687  tcvalg  9691  frmin  9702  scott0  9839  bnd2  9846  carduni  9934  cardaleph  10042  alephinit  10048  aceq3lem  10073  dfac12lem3  10099  infmap2  10170  cflem  10198  cflemOLD  10199  cflm  10203  cflecard  10206  cfeq0  10209  cfsuc  10210  cfflb  10212  cfslb  10219  cfslb2n  10221  coftr  10226  fin23lem13  10285  fin23lem16  10288  fin23lem19  10289  fin23lem29  10294  fin1a2lem13  10365  itunitc  10374  domtriomlem  10395  axdc3lem2  10404  zorn2lem7  10455  zornn0g  10458  pwfseqlem4a  10614  pwfseqlem4  10615  wunfi  10674  wunex2  10691  wuncval  10695  rankcf  10730  tskuni  10736  axgroth6  10781  axgroth3  10784  axgroth4  10785  fzoss1  13647  fsuppmapnn0fiubex  13957  hashf1lem2  14421  cleq1lem  14948  rtrclreclem4  15027  sumeq1  15655  fsumcvg3  15695  fsum2d  15737  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  prodeq1f  15872  prodeq1  15873  fprod2d  15947  lcmfunsnlem  16611  coprmprod  16631  vdwmc  16949  prmgaplem3  17024  prmgaplem4  17025  restsspw  17394  ismred2  17564  mrcval  17571  mrcuni  17582  acsfn  17620  isssc  17782  drsdirfi  18266  ipodrsima  18500  cntzssv  19260  pmtrfrn  19388  pmtrrn2  19390  pmtrdifellem1  19406  pmtrdifellem2  19407  sylow2alem2  19548  sylow2a  19549  efgval  19647  gsumzaddlem  19851  ablfac1eulem  20004  rgspnval  20521  lspval  20881  lspindpi  21042  znf1o  21461  zntoslem  21466  aspval  21782  mplsubglem  21908  mpllsslem  21909  mplcoe1  21944  mplcoe5  21947  mdetunilem9  22507  uniopn  22784  fiinopn  22788  fiinbas  22839  baspartn  22841  eltg2  22845  eltg3  22849  topbas  22859  pptbas  22895  clsval  22924  neiint  22991  neips  23000  opnneissb  23001  opnssneib  23002  innei  23012  neiptoptop  23018  neiptopnei  23019  restbas  23045  restcld  23059  neitr  23067  restcls  23068  restntr  23069  cnpdis  23180  cmpsublem  23286  cmpsub  23287  fiuncmp  23291  unconn  23316  1stcfb  23332  2ndc1stc  23338  1stcrest  23340  2ndcctbss  23342  2ndcomap  23345  dis2ndc  23347  lly1stc  23383  refssex  23398  refun0  23402  llycmpkgen2  23437  txbas  23454  eltx  23455  ptuni2  23463  neitx  23494  ptpjopn  23499  ptcld  23500  txlm  23535  tx1stc  23537  txkgen  23539  xkopt  23542  xkococnlem  23546  ptcmpfi  23700  fbssfi  23724  opnfbas  23729  isfil2  23743  isfildlem  23744  snfil  23751  fsubbas  23754  ssfg  23759  fgss2  23761  fgcl  23765  fbasrn  23771  fgtr  23777  ufli  23801  uffix  23808  rnelfmlem  23839  fclscf  23912  alexsublem  23931  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  tmdgsum2  23983  subgntr  23994  opnsubg  23995  qustgpopn  24007  tsmsfbas  24015  tsmsgsum  24026  tsmsres  24031  tsmsf1o  24032  tsmsxplem1  24040  tsmsxp  24042  isust  24091  ustssel  24093  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  ustexsym  24103  ust0  24107  restutop  24125  ustuqtop4  24132  utopsnneiplem  24135  blssexps  24314  blssex  24315  neibl  24389  blcld  24393  met1stc  24409  met2ndci  24410  metrest  24412  prdsxmslem2  24417  metustfbas  24445  cfilucfil  24447  metuel2  24453  metustbl  24454  restmetu  24458  dscopn  24461  isngp2  24485  tgioo  24684  tgqioo  24688  zdis  24705  xrge0tsms  24723  fsumcn  24761  volivth  25508  vitalilem2  25510  itgfsum  25728  limcun  25796  recnprss  25805  dvmptfsum  25879  ftc1a  25944  plyssc  26105  efopn  26567  jensen  26899  brsslt  27697  madef  27764  tglnunirn  28475  lpvtx  28995  umgredgprv  29034  usgredgprvALT  29122  issubgr2  29199  subgrprop2  29201  egrsubgr  29204  0uhgrsubgr  29206  frcond3  30198  hhsssh  31198  shintcl  31259  chintcl  31261  spanval  31262  omlsi  31333  pjoml  31365  chnlen0  31373  chsscon3  31429  chlejb1  31441  chnle  31443  spanun  31474  h1datom  31511  cmbr4i  31530  pjoml2  31540  pjoml3  31541  lecm  31546  osumcor2i  31573  osum  31574  spansncv  31582  pjcjt2  31621  pjopyth  31649  hstel2  32148  stj  32164  stcltr1i  32203  mdi  32224  mdbr3  32226  mdbr4  32227  dmdbr  32228  dmdmd  32229  dmdbr5  32237  mdsl1i  32250  mdslmd1lem3  32256  mdslmd1lem4  32257  mdslmd1i  32258  csmdsymi  32263  atss  32275  atom1d  32282  superpos  32283  chcv1  32284  shatomici  32287  shatomistici  32290  hatomistici  32291  chrelat2  32299  chirredi  32323  atcvat4i  32326  mdsymlem2  32333  mdsymlem6  32337  dmdbr6ati  32352  dmdbr7ati  32353  xrge0tsmsd  33002  gsumle  33038  gsumvsca1  33179  gsumvsca2  33180  prmidl  33411  ismxidl  33433  constrfiss  33741  zarcls1  33859  zarclsun  33860  zarclsiin  33861  zarclsint  33862  zarclssn  33863  zartop  33866  zartopon  33867  zart0  33869  zarmxt1  33870  zarcmp  33872  rhmpreimacnlem  33874  rhmpreimacn  33875  tpr2rico  33902  issiga  34102  isrnsiga  34103  sigagenval  34130  measiuns  34207  dya2icoseg  34268  dya2iocnrect  34272  dya2iocuni  34274  carsgmon  34305  carsgsigalem  34306  carsgclctunlem2  34310  carsgclctun  34312  pmeasmono  34315  pmeasadd  34316  bnj517  34875  bnj1118  34974  bnj1145  34983  bnj1154  34989  bnj1452  35042  bnj1498  35051  fineqvpow  35086  fineqvac  35087  fineqvacALT  35088  vonf1owev  35095  pthhashvtx  35115  kur14lem1  35193  cvmopnlem  35265  dfon2lem3  35773  dfon2lem7  35777  brsset  35877  fness  36337  fneref  36338  fnessref  36345  neibastop2lem  36348  topmeet  36352  fnejoin2  36357  tailfb  36365  filnetlem4  36369  onsucsuccmpi  36431  bj-snglss  36958  bj-elpwgALT  37042  bj-restpw  37080  bj-imdirco  37178  dissneqlem  37328  relowlssretop  37351  relowlpssretop  37352  ctbssinf  37394  pibt2  37405  matunitlindflem1  37610  ptrecube  37614  poimirlem29  37643  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  indexa  37727  indexdom  37728  neificl  37747  istotbnd3  37765  sstotbnd2  37768  sstotbnd  37769  equivtotbnd  37772  ssbnd  37782  heiborlem1  37805  heiborlem6  37810  heiborlem8  37812  heiborlem10  37814  unichnidl  38025  pridl  38031  ismaxidl  38034  igenval  38055  igenval2  38060  ispridlc  38064  relcnveq3  38309  iss2  38326  elrelscnveq3  38482  brssr  38492  lsmsat  39001  lssatomic  39004  lssats  39005  lsat0cv  39026  lcvexchlem4  39030  lcvexchlem5  39031  lsatcvatlem  39042  l1cvpat  39047  ispsubsp  39739  linepsubN  39746  pclvalN  39884  ispsubclN  39931  ispsubcl2N  39941  pclfinclN  39944  diaelrnN  41039  docavalN  41117  dochval  41345  dvh4dimat  41432  dochexmidlem1  41454  lpolconN  41481  mapdordlem2  41631  eqresfnbd  42220  ismrcd1  42686  ismrcd2  42687  ismrc  42689  mzpcompact2lem  42739  aomclem6  43048  hbtlem6  43118  onintunirab  43216  rp-brsslt  43412  ssficl  43558  ssuncl  43559  ssdifcl  43560  sssymdifcl  43561  elmapintrab  43565  clcnvlem  43612  iunrelexpmin1  43697  iunrelexpmin2  43701  clsk3nimkb  44029  clsk1indlem1  44034  isotone1  44037  isotone2  44038  ntrclsiso  44056  gneispace  44123  gneispacess2  44135  onfrALTlem5  44532  onfrALTlem5VD  44874  relpfrlem  44943  modelaxreplem1  44968  islptre  45617  dvmptconst  45913  dvmptidg  45915  dvmulcncf  45923  dvdivcncf  45925  dvmptfprod  45943  stoweidlem51  46049  stoweidlem52  46050  fourierdlem103  46207  fourierdlem104  46208  ioorrnopnlem  46302  ioorrnopnxrlem  46304  salgenval  46319  ovnval2  46543  ovncvrrp  46562  ovnsubaddlem1  46568  ovnsubadd  46570  ovncvr2  46609  hspmbl  46627  elsetpreimafvssdm  47387  isubgredg  47866  uhgrimisgrgriclem  47930  grimedg  47935  grtrissvtx  47943  grtrimap  47947  stgredgiun  47957  isubgr3stgrlem6  47970  isubgr3stgrlem7  47971  uspgrlimlem1  47987  uspgrlimlem2  47988  uspgrlimlem3  47989  uspgrlimlem4  47990  grlimgrtrilem1  47993  grlimgrtrilem2  47994  grlimgrtri  47995  usgrexmpl1lem  48012  usgrexmpl2lem  48017  uspgrsprfo  48136  unilbss  48806  sepfsepc  48916  unilbeu  48973  ipolubdm  48975  ipoglbdm  48978  discsubc  49053  iinfconstbas  49055  setrec1lem1  49676  setrec1lem4  49679  setrec2fun  49681  elsetrecslem  49688  elpglem2  49701