Theorem sseq1 3491

Description: Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

Ref	Expression
sseq1	|- ( A = B -> ( A C_ C <-> B C_ C ) )

Proof of Theorem sseq1

Step	Hyp	Ref	Expression
1		eqss 3485	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3477	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 467	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3477	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 466	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( B C_ C -> A C_ C ) )
6	3, 5	impbid 193	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
7	1, 6	sylbi 198	1 |- ( A = B -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   C_ wss 3442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456

This theorem is referenced by:  sseq12  3493  sseq1i  3494  sseq1d  3497  nssne2  3527  psseq1  3558  uneqdifeq  3890  sbss  3913  pwjust  3986  elpw  3991  elpwg  3993  pwpw0  4151  sssn  4161  ssunsn2  4162  pwsnALT  4217  unimax  4257  trss  4529  sseliALT  4558  elssabg  4580  intabs  4586  nnullss  4684  exss  4685  fri  4816  releq  4937  iss  5172  relcnvtr  5375  fununi  5667  ssimaex  5946  isofrlem  6246  onssmin  6638  tfis  6695  tfisi  6699  funcnvuni  6760  ffoss  6768  f1oweALT  6791  frxp  6917  wfrlem1  7043  wfrlem4  7047  wfrlem15  7058  tfrlem1  7102  oawordeu  7264  qsss  7432  boxcutc  7573  sbthlem2  7689  sbth  7698  php  7762  isinf  7791  findcard2d  7819  unbnn2  7834  domunfican  7850  fiint  7854  finsschain  7887  indexfi  7888  dffi3  7951  hartogslem1  8057  cantnfval2  8173  cantnfle  8175  cantnflem1  8193  tz9.1  8212  setind  8217  tcvalg  8221  scott0  8356  bnd2  8363  carduni  8414  cardaleph  8518  alephinit  8524  aceq3lem  8549  dfac12lem3  8573  infmap2  8646  cflem  8674  cflm  8678  cflecard  8681  cfeq0  8684  cfsuc  8685  cfflb  8687  cfslb  8694  cfslb2n  8696  coftr  8701  fin23lem13  8760  fin23lem16  8763  fin23lem19  8764  fin23lem29  8769  fin1a2lem13  8840  itunitc  8849  domtriomlem  8870  axdc3lem2  8879  zorn2lem7  8930  zornn0g  8933  fpwwe2lem5  9058  pwfseqlem4a  9085  pwfseqlem4  9086  wunfi  9145  wunex2  9162  wuncval  9166  rankcf  9201  tskuni  9207  axgroth6  9252  axgroth3  9255  axgroth4  9256  fzoss1  11943  fsuppmapnn0fiubex  12201  hashf1lem2  12614  cleq1lem  13025  rtrclreclem4  13103  sumeq1  13733  fsumcvg3  13773  fsum2d  13810  fsumabs  13839  fsumrlim  13849  fsumo1  13850  fsumiun  13859  prodeq1f  13940  fprod2d  14013  lcmfunsnlem  14585  coprmprod  14649  vdwmc  14891  prmgaplem3  14986  prmgaplem4  14987  restsspw  15289  ismred2  15460  mrcval  15467  mrcuni  15478  acsfn  15516  isssc  15676  drsdirfi  16134  ipodrsima  16362  cntzssv  16933  pmtrfrn  17050  pmtrrn2  17052  pmtrdifellem1  17068  pmtrdifellem2  17069  isslw  17195  sylow2alem2  17205  sylow2a  17206  efgval  17302  gsumzaddlem  17489  ablfac1eulem  17640  lspval  18133  lspindpi  18290  aspval  18487  mplsubglem  18593  mpllsslem  18594  mplcoe1  18624  mplcoe5  18627  znf1o  19053  zntoslem  19058  mdetunilem9  19576  uniopn  19858  fiinopn  19862  fiinbas  19898  baspartn  19900  eltg2  19904  eltg3  19908  topbas  19919  pptbas  19954  clsval  19983  neival  20049  neiint  20051  neips  20060  opnneissb  20061  opnssneib  20062  innei  20072  neiptoptop  20078  neiptopnei  20079  restbas  20105  restcld  20119  neitr  20127  restcls  20128  restntr  20129  cnpdis  20240  nrmsep3  20302  cmpsublem  20345  cmpsub  20346  fiuncmp  20350  uncon  20375  1stcfb  20391  2ndc1stc  20397  1stcrest  20399  2ndcctbss  20401  2ndcomap  20404  dis2ndc  20406  lly1stc  20442  refssex  20457  refun0  20461  llycmpkgen2  20496  txbas  20513  eltx  20514  ptuni2  20522  neitx  20553  ptpjopn  20558  ptcld  20559  txlm  20594  tx1stc  20596  txkgen  20598  xkopt  20601  xkococnlem  20605  ptcmpfi  20759  fbssfi  20783  opnfbas  20788  isfil2  20802  isfildlem  20803  snfil  20810  fsubbas  20813  ssfg  20818  fgss2  20820  fgcl  20824  fbasrn  20830  fgtr  20836  ufli  20860  uffix  20867  rnelfmlem  20898  fclscf  20971  alexsublem  20990  alexsubALTlem2  20994  alexsubALTlem3  20995  alexsubALTlem4  20996  alexsubALT  20997  tmdgsum2  21042  subgntr  21052  opnsubg  21053  qustgpopn  21065  tsmsfbas  21073  tsmsgsum  21084  tsmsres  21089  tsmsf1o  21090  tsmsxplem1  21098  tsmsxp  21100  isust  21149  ustssel  21151  ustincl  21153  ustdiag  21154  ustinvel  21155  ustexhalf  21156  ustexsym  21161  ust0  21165  restutop  21183  ustuqtop4  21190  utopsnneiplem  21193  blssexps  21372  blssex  21373  neibl  21447  blcld  21451  met1stc  21467  met2ndci  21468  metrest  21470  prdsxmslem2  21475  metustfbas  21503  cfilucfil  21505  metuel2  21511  metustbl  21512  restmetu  21516  dscopn  21519  isngp2  21542  tgioo  21725  tgqioo  21729  zdis  21745  xrge0tsms  21763  fsumcn  21798  ovolval  22305  volivth  22442  vitalilem2  22444  itgfsum  22661  limcun  22727  recnprss  22736  dvmptfsum  22804  ftc1a  22866  plyssc  23022  efopn  23468  jensen  23779  tglnunirn  24453  usgraedgprv  24949  frisusgranb  25570  hhsssh  26755  shintcl  26818  chintcl  26820  spanval  26821  omlsi  26892  pjoml  26924  chnlen0  26932  chsscon3  26988  chlejb1  27000  chnle  27002  spanun  27033  h1datom  27070  cmbr4i  27089  pjoml2  27099  pjoml3  27100  lecm  27105  osumcor2i  27132  osum  27133  spansncv  27141  pjcjt2  27180  pjopyth  27208  hstel2  27707  stj  27723  stcltr1i  27762  mdi  27783  mdbr3  27785  mdbr4  27786  dmdbr  27787  dmdmd  27788  dmdbr5  27796  mdsl1i  27809  mdslmd1lem3  27815  mdslmd1lem4  27816  mdslmd1i  27817  csmdsymi  27822  atss  27834  atom1d  27841  superpos  27842  chcv1  27843  shatomici  27846  shatomistici  27849  hatomistici  27850  chrelat2  27858  chirredi  27882  atcvat4i  27885  mdsymlem2  27892  mdsymlem6  27896  dmdbr6ati  27911  dmdbr7ati  27912  gsumle  28380  gsumvsca1  28384  gsumvsca2  28385  xrge0tsmsd  28387  tpr2rico  28557  issiga  28772  isrnsigaOLD  28773  isrnsiga  28774  sigagenval  28801  measiuns  28878  dya2icoseg  28938  dya2iocnrect  28942  dya2iocuni  28944  carsgmon  28975  carsgsigalem  28976  carsgclctunlem2  28980  carsgclctun  28982  pmeasmono  28985  pmeasadd  28986  bnj517  29484  bnj1118  29581  bnj1145  29590  bnj1154  29596  bnj1452  29649  bnj1498  29658  kur14lem1  29717  cvmopnlem  29789  dfon2lem3  30218  dfon2lem7  30222  frmin  30267  frrlem1  30301  frrlem3  30303  brsset  30441  fness  30790  fneref  30791  fnessref  30798  neibastop2lem  30801  topmeet  30805  fnejoin2  30810  tailfb  30818  filnetlem4  30822  onsucsuccmpi  30888  bj-snglss  31313  dissneqlem  31476  relowlssretop  31500  relowlpssretop  31501  ptrecube  31643  poimirlem29  31672  mblfinlem2  31681  mblfinlem3  31682  mblfinlem4  31683  ismblfin  31684  ovoliunnfl  31685  voliunnfl  31687  volsupnfl  31688  indexa  31763  indexdom  31764  neificl  31785  istotbnd3  31806  sstotbnd2  31809  sstotbnd  31810  equivtotbnd  31813  ssbnd  31823  heiborlem1  31846  heiborlem6  31851  heiborlem8  31853  heiborlem10  31855  unichnidl  31967  pridl  31973  ismaxidl  31976  igenval  31997  igenval2  32002  ispridlc  32006  lsmsat  32282  lssatomic  32285  lssats  32286  lsat0cv  32307  lcvexchlem4  32311  lcvexchlem5  32312  lsatcvatlem  32323  l1cvpat  32328  ispsubsp  33018  linepsubN  33025  pclvalN  33163  ispsubclN  33210  ispsubcl2N  33220  pclfinclN  33223  diaelrnN  34321  docavalN  34399  dochval  34627  dvh4dimat  34714  dochexmidlem1  34736  lpolconN  34763  mapdordlem2  34913  ismrcd1  35248  ismrcd2  35249  ismrc  35251  mzpcompact2lem  35301  aomclem6  35622  hbtlem6  35693  rgspnval  35732  ssficl  35871  ssuncl  35872  ssdifcl  35873  sssymdifcl  35874  iunrelexpmin1  35938  iunrelexpmin2  35942  onfrALTlem5  36544  onfrALTlem5VD  36921  islptre  37270  dvmptconst  37356  dvmptidg  37358  dvmulcncf  37368  dvdivcncf  37370  dvmptfprod  37388  stoweidlem51  37480  stoweidlem52  37481  fourierdlem103  37640  fourierdlem104  37641