Theorem sseq1 3365

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 3359	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3351	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 463	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3351	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 462	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( B C_ C -> A C_ C ) )
6	3, 5	impbid 191	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
7	1, 6	sylbi 195	1 |- ( A = B -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1362   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330

This theorem is referenced by:  sseq12  3367  sseq1i  3368  sseq1d  3371  nssne2  3401  psseq1  3431  uneqdifeq  3755  sbss  3777  pwjust  3849  elpw  3854  elpwg  3856  pwpw0  4009  sssn  4019  ssunsn2  4020  pwsnALT  4074  unimax  4115  trss  4382  sseliALT  4411  elssabg  4435  intabs  4441  nnullss  4542  exss  4543  fri  4669  releq  4909  xpsspw  4940  iss  5142  relcnvtr  5345  fununi  5472  ssimaex  5744  isofrlem  6018  onssmin  6397  tfis  6454  tfisi  6458  funcnvuni  6519  ffoss  6527  f1oweALT  6550  frxp  6671  tfrlem1  6821  oawordeu  6982  qsss  7149  boxcutc  7294  sbthlem2  7410  sbth  7419  php  7483  isinf  7514  findcard2d  7542  unbnn2  7557  domunfican  7572  fiint  7576  finsschain  7606  indexfi  7607  dffi3  7669  hartogslem1  7744  sucprcregOLD  7803  cantnfval2  7865  cantnfle  7867  cantnflem1  7885  cantnfval2OLD  7895  cantnfleOLD  7897  cantnflem1OLD  7908  tz9.1  7937  setind  7942  tcvalg  7946  scott0  8081  bnd2  8088  carduni  8139  cardaleph  8247  alephinit  8253  aceq3lem  8278  dfac12lem3  8302  infmap2  8375  cflem  8403  cflm  8407  cflecard  8410  cfeq0  8413  cfsuc  8414  cfflb  8416  cfslb  8423  cfslb2n  8425  coftr  8430  fin23lem13  8489  fin23lem16  8492  fin23lem19  8493  fin23lem29  8498  fin1a2lem13  8569  itunitc  8578  domtriomlem  8599  axdc3lem2  8608  zorn2lem7  8659  zornn0g  8662  fpwwe2lem5  8789  pwfseqlem4a  8816  pwfseqlem4  8817  wunfi  8876  wunex2  8893  wuncval  8897  rankcf  8932  tskuni  8938  axgroth6  8983  axgroth3  8986  axgroth4  8987  fzoss1  11560  hashf1lem2  12193  sumeq1  13150  fsumcvg3  13190  fsum2d  13222  fsumabs  13247  fsumrlim  13257  fsumo1  13258  fsumiun  13267  vdwmc  14022  restsspw  14353  ismred2  14524  mrcval  14531  mrcuni  14542  acsfn  14580  isssc  14716  drsdirfi  15091  ipodrsima  15318  cntzssv  15826  pmtrfrn  15944  pmtrrn2  15946  pmtrdifellem1  15962  pmtrdifellem2  15963  isslw  16087  sylow2alem2  16097  sylow2a  16098  efgval  16194  gsumzaddlem  16388  gsumzaddlemOLD  16390  ablfac1eulem  16547  lspval  16978  lspindpi  17135  aspval  17321  mplsubglem  17444  mpllsslem  17445  mplsubglemOLD  17446  mpllsslemOLD  17447  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  znf1o  17826  zntoslem  17831  mdetunilem9  18268  uniopn  18352  fiinopn  18356  fiinbas  18399  baspartn  18401  eltg2  18405  eltg3  18409  topbas  18419  pptbas  18454  clsval  18483  neival  18548  neiint  18550  neips  18559  opnneissb  18560  opnssneib  18561  innei  18571  neiptoptop  18577  neiptopnei  18578  restbas  18604  restcld  18618  neitr  18626  restcls  18627  restntr  18628  cnpdis  18739  nrmsep3  18801  cmpsublem  18844  cmpsub  18845  fiuncmp  18849  uncon  18875  1stcfb  18891  2ndc1stc  18897  1stcrest  18899  2ndcctbss  18901  2ndcomap  18904  dis2ndc  18906  lly1stc  18942  llycmpkgen2  18965  txbas  18982  eltx  18983  ptuni2  18991  neitx  19022  ptpjopn  19027  ptcld  19028  txlm  19063  tx1stc  19065  txkgen  19067  xkopt  19070  xkococnlem  19074  ptcmpfi  19228  fbssfi  19252  opnfbas  19257  isfil2  19271  isfildlem  19272  snfil  19279  fsubbas  19282  ssfg  19287  fgss2  19289  fgcl  19293  fbasrn  19299  fgtr  19305  ufli  19329  uffix  19336  rnelfmlem  19367  fclscf  19440  alexsublem  19458  alexsubALTlem2  19462  alexsubALTlem3  19463  alexsubALTlem4  19464  alexsubALT  19465  tmdgsum2  19509  subgntr  19519  opnsubg  19520  divstgpopn  19532  tsmsfbas  19540  tsmsgsum  19551  tsmsgsumOLD  19554  tsmsresOLD  19559  tsmsres  19560  tsmsf1o  19561  tsmsxplem1  19569  tsmsxp  19571  isust  19620  ustssel  19622  ustincl  19624  ustdiag  19625  ustinvel  19626  ustexhalf  19627  ustexsym  19632  ust0  19636  restutop  19654  ustuqtop4  19661  utopsnneiplem  19664  blssexps  19843  blssex  19844  neibl  19918  blcld  19922  met1stc  19938  met2ndci  19939  metrest  19941  prdsxmslem2  19946  metustfbasOLD  19982  metustfbas  19983  cfilucfilOLD  19986  cfilucfil  19987  metuel2  19996  metustblOLD  19997  metustbl  19998  restmetu  20004  dscopn  20008  isngp2  20031  tgioo  20215  tgqioo  20219  zdis  20235  xrge0tsms  20253  fsumcn  20288  ovolval  20799  volivth  20929  vitalilem2  20931  itgfsum  21146  limcun  21212  recnprss  21221  dvmptfsum  21289  ftc1a  21351  plyssc  21553  efopn  21988  jensen  22267  tglnunirn  22863  usgraedgprv  23118  hhsssh  24493  shintcl  24556  chintcl  24558  spanval  24559  omlsi  24630  pjoml  24662  chnlen0  24670  chsscon3  24726  chlejb1  24738  chnle  24740  spanun  24771  h1datom  24808  cmbr4i  24827  pjoml2  24837  pjoml3  24838  lecm  24843  osumcor2i  24870  osum  24871  spansncv  24879  pjcjt2  24918  pjopyth  24946  hstel2  25446  stj  25462  stcltr1i  25501  mdi  25522  mdbr3  25524  mdbr4  25525  dmdbr  25526  dmdmd  25527  dmdbr5  25535  mdsl1i  25548  mdslmd1lem3  25554  mdslmd1lem4  25555  mdslmd1i  25556  csmdsymi  25561  atss  25573  atom1d  25580  superpos  25581  chcv1  25582  shatomici  25585  shatomistici  25588  hatomistici  25589  chrelat2  25597  chirredi  25621  atcvat4i  25624  mdsymlem2  25631  mdsymlem6  25635  dmdbr6ati  25650  dmdbr7ati  25651  gsumle  26098  gsumvsca1  26104  gsumvsca2  26105  xrge0tsmsd  26106  tpr2rico  26196  issiga  26408  isrnsigaOLD  26409  isrnsiga  26410  sigagenval  26437  measiuns  26485  dya2icoseg  26546  dya2iocnrect  26550  dya2iocuni  26552  kur14lem1  26942  cvmopnlem  27015  rtrclreclem.min  27196  prodeq1f  27268  fprod2d  27339  dfon2lem3  27445  dfon2lem7  27449  frmin  27550  wfrlem1  27571  wfrlem4  27574  wfrlem15  27585  frrlem1  27615  frrlem3  27617  brsset  27767  onsucsuccmpi  28137  mblfinlem2  28273  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  ovoliunnfl  28277  voliunnfl  28279  volsupnfl  28280  refssex  28397  fness  28398  fneref  28400  fnessref  28409  neibastop2lem  28425  topmeet  28429  fnejoin2  28434  tailfb  28442  filnetlem4  28446  indexa  28471  indexdom  28472  neificl  28493  istotbnd3  28514  sstotbnd2  28517  sstotbnd  28518  equivtotbnd  28521  ssbnd  28531  heiborlem1  28554  heiborlem6  28559  heiborlem8  28561  heiborlem10  28563  unichnidl  28675  pridl  28681  ismaxidl  28684  igenval  28705  igenval2  28710  ispridlc  28714  ismrcd1  28879  ismrcd2  28880  ismrc  28882  mzpcompact2lem  28933  aomclem6  29257  hbtlem6  29330  rgspnval  29370  stoweidlem51  29692  stoweidlem52  29693  frisusgranb  30435  onfrALTlem5  30951  onfrALTlem5VD  31323  bnj517  31580  bnj1118  31677  bnj1145  31686  bnj1154  31692  bnj1452  31745  bnj1498  31754  bj-snglss  32046  lsmsat  32226  lssatomic  32229  lssats  32230  lsat0cv  32251  lcvexchlem4  32255  lcvexchlem5  32256  lsatcvatlem  32267  l1cvpat  32272  ispsubsp  32962  linepsubN  32969  pclvalN  33107  ispsubclN  33154  ispsubcl2N  33164  pclfinclN  33167  diaelrnN  34263  docavalN  34341  dochval  34569  dvh4dimat  34656  dochexmidlem1  34678  lpolconN  34705  mapdordlem2  34855