Theorem sseq1 3329

Description: Equality theorem for subclasses. (Contributed by NM, 5-Aug-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 3323	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3315	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 453	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3315	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 452	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( B C_ C -> A C_ C ) )
6	3, 5	impbid 184	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
7	1, 6	sylbi 188	1 |- ( A = B -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   C_ wss 3280

This theorem is referenced by:  sseq12  3331  sseq1i  3332  sseq1d  3335  nssne2  3365  psseq1  3394  uneqdifeq  3676  sbss  3697  pwjust  3760  elpw  3765  elpwg  3766  pwpw0  3906  sssn  3917  ssunsn2  3918  pwsnALT  3970  unimax  4009  trss  4271  elssabg  4315  intabs  4321  nnullss  4385  exss  4386  fri  4504  onssmin  4736  tfis  4793  tfisi  4797  releq  4918  xpsspw  4945  iss  5148  relcnvtr  5348  fununi  5476  funcnvuni  5477  ffoss  5666  ssimaex  5747  isofrlem  6019  f1oweALT  6033  frxp  6415  tfrlem1  6595  oawordeu  6757  qsss  6924  boxcutc  7064  sbthlem2  7177  sbth  7186  php  7250  isinf  7281  unbnn2  7323  domunfican  7338  fiint  7342  finsschain  7371  indexfi  7372  dffi3  7394  hartogslem1  7467  sucprcreg  7523  cantnfval2  7580  cantnfle  7582  cantnflem1  7601  tz9.1  7621  setind  7629  tcvalg  7633  scott0  7766  bnd2  7773  carduni  7824  cardaleph  7926  alephinit  7932  aceq3lem  7957  dfac12lem3  7981  infmap2  8054  cflem  8082  cflm  8086  cflecard  8089  cfeq0  8092  cfsuc  8093  cfflb  8095  cfslb  8102  cfslb2n  8104  coftr  8109  fin23lem13  8168  fin23lem16  8171  fin23lem19  8172  fin23lem29  8177  fin1a2lem13  8248  itunitc  8257  domtriomlem  8278  axdc3lem2  8287  zorn2lem7  8338  zornn0g  8341  fpwwe2lem5  8465  pwfseqlem4a  8492  pwfseqlem4  8493  wunfi  8552  wunex2  8569  wuncval  8573  rankcf  8608  tskuni  8614  axgroth6  8659  axgroth3  8662  axgroth4  8663  fzoss1  11117  hashf1lem2  11660  sumeq1f  12437  fsumcvg3  12478  fsum2d  12510  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  vdwmc  13301  restsspw  13614  ismred2  13783  mrcval  13790  mrcuni  13801  acsfn  13839  isssc  13975  drsdirfi  14350  clatlem  14494  clatl  14498  ipodrsima  14546  cntzssv  15082  isslw  15197  sylow2alem2  15207  sylow2a  15208  efgval  15304  gsumzaddlem  15481  ablfac1eulem  15585  lspval  16006  lspindpi  16159  aspval  16342  mplsubglem  16453  mpllsslem  16454  mplcoe1  16483  mplcoe2  16485  znf1o  16787  zntoslem  16792  uniopn  16925  fiinopn  16929  fiinbas  16972  baspartn  16974  eltg2  16978  eltg3  16982  topbas  16992  pptbas  17027  clsval  17056  neival  17121  neiint  17123  neips  17132  opnneissb  17133  opnssneib  17134  innei  17144  neiptoptop  17150  neiptopnei  17151  restbas  17176  restcld  17190  neitr  17198  restcls  17199  restntr  17200  cnpdis  17311  nrmsep3  17373  cmpsublem  17416  cmpsub  17417  fiuncmp  17421  uncon  17445  1stcfb  17461  2ndc1stc  17467  1stcrest  17469  2ndcctbss  17471  2ndcomap  17474  dis2ndc  17476  lly1stc  17512  llycmpkgen2  17535  txbas  17552  eltx  17553  ptuni2  17561  neitx  17592  ptpjopn  17597  ptcld  17598  txlm  17633  tx1stc  17635  txkgen  17637  xkopt  17640  xkococnlem  17644  ptcmpfi  17798  fbssfi  17822  opnfbas  17827  isfil2  17841  isfildlem  17842  snfil  17849  fsubbas  17852  ssfg  17857  fgss2  17859  fgcl  17863  fbasrn  17869  fgtr  17875  ufli  17899  uffix  17906  rnelfmlem  17937  fclscf  18010  alexsublem  18028  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  tmdgsum2  18079  subgntr  18089  opnsubg  18090  divstgpopn  18102  tsmsfbas  18110  tsmsgsum  18121  tsmsres  18126  tsmsf1o  18127  tsmsxplem1  18135  tsmsxp  18137  isust  18186  ustssel  18188  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  ustexsym  18198  ust0  18202  restutop  18220  ustuqtop4  18227  utopsnneiplem  18230  blssexps  18409  blssex  18410  neibl  18484  blcld  18488  met1stc  18504  met2ndci  18505  metrest  18507  prdsxmslem2  18512  metustfbasOLD  18548  metustfbas  18549  cfilucfilOLD  18552  cfilucfil  18553  metuel2  18562  metustblOLD  18563  metustbl  18564  restmetu  18570  dscopn  18574  isngp2  18597  tgioo  18780  tgqioo  18784  zdis  18800  xrge0tsms  18818  fsumcn  18853  ovolval  19323  volivth  19452  vitalilem2  19454  itgfsum  19671  limcun  19735  recnprss  19744  dvmptfsum  19812  ftc1a  19874  plyssc  20072  efopn  20502  jensen  20780  usgraedgprv  21349  hhsssh  22722  shintcl  22785  chintcl  22787  spanval  22788  omlsi  22859  pjoml  22891  chnlen0  22899  chsscon3  22955  chlejb1  22967  chnle  22969  spanun  23000  h1datom  23037  cmbr4i  23056  pjoml2  23066  pjoml3  23067  lecm  23072  osumcor2i  23099  osum  23100  spansncv  23108  pjcjt2  23147  pjopyth  23175  hstel2  23675  stj  23691  stcltr1i  23730  mdi  23751  mdbr3  23753  mdbr4  23754  dmdbr  23755  dmdmd  23756  dmdbr5  23764  mdsl1i  23777  mdslmd1lem3  23783  mdslmd1lem4  23784  mdslmd1i  23785  csmdsymi  23790  atss  23802  atom1d  23809  superpos  23810  chcv1  23811  shatomici  23814  shatomistici  23817  hatomistici  23818  chrelat2  23826  chirredi  23850  atcvat4i  23853  mdsymlem2  23860  mdsymlem6  23864  dmdbr6ati  23879  dmdbr7ati  23880  xrge0tsmsd  24176  tpr2rico  24263  issiga  24447  isrnsigaOLD  24448  isrnsiga  24449  sigagenval  24476  measiuns  24524  dya2icoseg  24580  dya2iocnrect  24584  dya2iocuni  24586  kur14lem1  24845  cvmopnlem  24918  rtrclreclem.min  25100  prodeq1f  25187  fprod2d  25258  dfon2lem3  25355  dfon2lem7  25359  frmin  25456  wfrlem1  25470  wfrlem4  25473  wfrlem15  25484  frrlem1  25495  frrlem3  25497  brsset  25643  bpolyval  25999  onsucsuccmpi  26097  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  refssex  26251  fness  26252  fneref  26254  fnessref  26263  neibastop2lem  26279  topmeet  26283  fnejoin2  26288  tailfb  26296  filnetlem4  26300  indexa  26325  indexdom  26326  neificl  26349  istotbnd3  26370  sstotbnd2  26373  sstotbnd  26374  equivtotbnd  26377  ssbnd  26387  heiborlem1  26410  heiborlem6  26415  heiborlem8  26417  heiborlem10  26419  unichnidl  26531  pridl  26537  ismaxidl  26540  igenval  26561  igenval2  26566  ispridlc  26570  ismrcd1  26642  ismrcd2  26643  ismrc  26645  mzpcompact2lem  26698  aomclem6  27024  hbtlem6  27201  rgspnval  27241  pmtrfrn  27268  stoweidlem51  27667  stoweidlem52  27668  frisusgranb  28101  onfrALTlem5  28339  onfrALTlem5VD  28706  bnj517  28962  bnj1118  29059  bnj1145  29068  bnj1154  29074  bnj1452  29127  bnj1498  29136  lsmsat  29491  lssatomic  29494  lssats  29495  lsat0cv  29516  lcvexchlem4  29520  lcvexchlem5  29521  lsatcvatlem  29532  l1cvpat  29537  ispsubsp  30227  linepsubN  30234  pclvalN  30372  ispsubclN  30419  ispsubcl2N  30429  pclfinclN  30432  diaelrnN  31528  docavalN  31606  dochval  31834  dvh4dimat  31921  dochexmidlem1  31943  lpolconN  31970  mapdordlem2  32120

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294