Theorem sseq1 3485

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 3479	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3471	. . . 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 3471	. . . 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 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450

This theorem is referenced by:  sseq12  3487  sseq1i  3488  sseq1d  3491  nssne2  3521  psseq1  3552  uneqdifeq  3886  sbss  3909  pwjust  3982  elpw  3987  elpwg  3989  pwpw0  4148  sssn  4158  ssunsn2  4159  pwsnALT  4214  unimax  4254  trss  4527  sseliALT  4557  elssabg  4579  intabs  4585  nnullss  4683  exss  4684  fri  4815  releq  4936  iss  5171  relcnvtr  5374  fununi  5667  ssimaex  5946  isofrlem  6246  onssmin  6638  tfis  6695  tfisi  6699  funcnvuni  6760  ffoss  6768  f1oweALT  6791  frxp  6917  wfrlem1  7046  wfrlem4  7050  wfrlem15  7061  tfrlem1  7105  oawordeu  7267  qsss  7435  boxcutc  7576  sbthlem2  7692  sbth  7701  php  7765  isinf  7794  findcard2d  7822  unbnn2  7837  domunfican  7853  fiint  7857  finsschain  7890  indexfi  7891  dffi3  7954  hartogslem1  8066  cantnfval2  8182  cantnfle  8184  cantnflem1  8202  tz9.1  8221  setind  8226  tcvalg  8230  scott0  8365  bnd2  8372  carduni  8423  cardaleph  8527  alephinit  8533  aceq3lem  8558  dfac12lem3  8582  infmap2  8655  cflem  8683  cflm  8687  cflecard  8690  cfeq0  8693  cfsuc  8694  cfflb  8696  cfslb  8703  cfslb2n  8705  coftr  8710  fin23lem13  8769  fin23lem16  8772  fin23lem19  8773  fin23lem29  8778  fin1a2lem13  8849  itunitc  8858  domtriomlem  8879  axdc3lem2  8888  zorn2lem7  8939  zornn0g  8942  fpwwe2lem5  9066  pwfseqlem4a  9093  pwfseqlem4  9094  wunfi  9153  wunex2  9170  wuncval  9174  rankcf  9209  tskuni  9215  axgroth6  9260  axgroth3  9263  axgroth4  9264  fzoss1  11952  fsuppmapnn0fiubex  12210  hashf1lem2  12623  cleq1lem  13046  rtrclreclem4  13124  sumeq1  13754  fsumcvg3  13794  fsum2d  13831  fsumabs  13860  fsumrlim  13870  fsumo1  13871  fsumiun  13880  prodeq1f  13961  fprod2d  14034  lcmfunsnlem  14613  coprmprod  14677  vdwmc  14927  prmgaplem3  15022  prmgaplem4  15023  restsspw  15329  ismred2  15508  mrcval  15515  mrcuni  15526  acsfn  15564  isssc  15724  drsdirfi  16182  ipodrsima  16410  cntzssv  16981  pmtrfrn  17098  pmtrrn2  17100  pmtrdifellem1  17116  pmtrdifellem2  17117  isslw  17259  sylow2alem2  17269  sylow2a  17270  efgval  17366  gsumzaddlem  17553  ablfac1eulem  17704  lspval  18197  lspindpi  18354  aspval  18551  mplsubglem  18657  mpllsslem  18658  mplcoe1  18688  mplcoe5  18691  znf1o  19120  zntoslem  19125  mdetunilem9  19643  uniopn  19925  fiinopn  19929  fiinbas  19965  baspartn  19967  eltg2  19971  eltg3  19975  topbas  19986  pptbas  20021  clsval  20050  neival  20116  neiint  20118  neips  20127  opnneissb  20128  opnssneib  20129  innei  20139  neiptoptop  20145  neiptopnei  20146  restbas  20172  restcld  20186  neitr  20194  restcls  20195  restntr  20196  cnpdis  20307  nrmsep3  20369  cmpsublem  20412  cmpsub  20413  fiuncmp  20417  uncon  20442  1stcfb  20458  2ndc1stc  20464  1stcrest  20466  2ndcctbss  20468  2ndcomap  20471  dis2ndc  20473  lly1stc  20509  refssex  20524  refun0  20528  llycmpkgen2  20563  txbas  20580  eltx  20581  ptuni2  20589  neitx  20620  ptpjopn  20625  ptcld  20626  txlm  20661  tx1stc  20663  txkgen  20665  xkopt  20668  xkococnlem  20672  ptcmpfi  20826  fbssfi  20850  opnfbas  20855  isfil2  20869  isfildlem  20870  snfil  20877  fsubbas  20880  ssfg  20885  fgss2  20887  fgcl  20891  fbasrn  20897  fgtr  20903  ufli  20927  uffix  20934  rnelfmlem  20965  fclscf  21038  alexsublem  21057  alexsubALTlem2  21061  alexsubALTlem3  21062  alexsubALTlem4  21063  alexsubALT  21064  tmdgsum2  21109  subgntr  21119  opnsubg  21120  qustgpopn  21132  tsmsfbas  21140  tsmsgsum  21151  tsmsres  21156  tsmsf1o  21157  tsmsxplem1  21165  tsmsxp  21167  isust  21216  ustssel  21218  ustincl  21220  ustdiag  21221  ustinvel  21222  ustexhalf  21223  ustexsym  21228  ust0  21232  restutop  21250  ustuqtop4  21257  utopsnneiplem  21260  blssexps  21439  blssex  21440  neibl  21514  blcld  21518  met1stc  21534  met2ndci  21535  metrest  21537  prdsxmslem2  21542  metustfbas  21570  cfilucfil  21572  metuel2  21578  metustbl  21579  restmetu  21583  dscopn  21586  isngp2  21609  tgioo  21812  tgqioo  21816  zdis  21832  xrge0tsms  21850  fsumcn  21900  ovolval  22424  ovolvalOLD  22425  volivth  22563  vitalilem2  22565  itgfsum  22782  limcun  22848  recnprss  22857  dvmptfsum  22925  ftc1a  22987  plyssc  23152  efopn  23601  jensen  23912  tglnunirn  24591  usgraedgprv  25101  frisusgranb  25723  hhsssh  26918  shintcl  26981  chintcl  26983  spanval  26984  omlsi  27055  pjoml  27087  chnlen0  27095  chsscon3  27151  chlejb1  27163  chnle  27165  spanun  27196  h1datom  27233  cmbr4i  27252  pjoml2  27262  pjoml3  27263  lecm  27268  osumcor2i  27295  osum  27296  spansncv  27304  pjcjt2  27343  pjopyth  27371  hstel2  27870  stj  27886  stcltr1i  27925  mdi  27946  mdbr3  27948  mdbr4  27949  dmdbr  27950  dmdmd  27951  dmdbr5  27959  mdsl1i  27972  mdslmd1lem3  27978  mdslmd1lem4  27979  mdslmd1i  27980  csmdsymi  27985  atss  27997  atom1d  28004  superpos  28005  chcv1  28006  shatomici  28009  shatomistici  28012  hatomistici  28013  chrelat2  28021  chirredi  28045  atcvat4i  28048  mdsymlem2  28055  mdsymlem6  28059  dmdbr6ati  28074  dmdbr7ati  28075  gsumle  28549  gsumvsca1  28553  gsumvsca2  28554  xrge0tsmsd  28556  tpr2rico  28726  issiga  28941  isrnsigaOLD  28942  isrnsiga  28943  sigagenval  28970  measiuns  29047  dya2icoseg  29107  dya2iocnrect  29111  dya2iocuni  29113  carsgmon  29154  carsgsigalem  29155  carsgclctunlem2  29159  carsgclctun  29161  pmeasmono  29165  pmeasadd  29166  bnj517  29704  bnj1118  29801  bnj1145  29810  bnj1154  29816  bnj1452  29869  bnj1498  29878  kur14lem1  29937  cvmopnlem  30009  dfon2lem3  30438  dfon2lem7  30442  frmin  30487  frrlem1  30521  frrlem3  30523  brsset  30661  fness  31010  fneref  31011  fnessref  31018  neibastop2lem  31021  topmeet  31025  fnejoin2  31030  tailfb  31038  filnetlem4  31042  onsucsuccmpi  31108  bj-snglss  31532  dissneqlem  31706  relowlssretop  31730  relowlpssretop  31731  ptrecube  31904  poimirlem29  31933  mblfinlem2  31942  mblfinlem3  31943  mblfinlem4  31944  ismblfin  31945  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  indexa  32024  indexdom  32025  neificl  32046  istotbnd3  32067  sstotbnd2  32070  sstotbnd  32071  equivtotbnd  32074  ssbnd  32084  heiborlem1  32107  heiborlem6  32112  heiborlem8  32114  heiborlem10  32116  unichnidl  32228  pridl  32234  ismaxidl  32237  igenval  32258  igenval2  32263  ispridlc  32267  lsmsat  32543  lssatomic  32546  lssats  32547  lsat0cv  32568  lcvexchlem4  32572  lcvexchlem5  32573  lsatcvatlem  32584  l1cvpat  32589  ispsubsp  33279  linepsubN  33286  pclvalN  33424  ispsubclN  33471  ispsubcl2N  33481  pclfinclN  33484  diaelrnN  34582  docavalN  34660  dochval  34888  dvh4dimat  34975  dochexmidlem1  34997  lpolconN  35024  mapdordlem2  35174  ismrcd1  35509  ismrcd2  35510  ismrc  35512  mzpcompact2lem  35562  aomclem6  35887  hbtlem6  35958  rgspnval  36004  ssficl  36143  ssuncl  36144  ssdifcl  36145  sssymdifcl  36146  elmapintrab  36152  clcnvlem  36200  iunrelexpmin1  36270  iunrelexpmin2  36274  onfrALTlem5  36878  onfrALTlem5VD  37255  islptre  37639  dvmptconst  37725  dvmptidg  37727  dvmulcncf  37737  dvdivcncf  37739  dvmptfprod  37760  stoweidlem51  37852  stoweidlem52  37853  fourierdlem103  38013  fourierdlem104  38014  ovnval2  38271  ovncvrrp  38290  ovnsubaddlem1  38296  ovnsubadd  38298  usgredgprv  39066  issubgr2  39118  subgrprop2  39120  egrsubgr  39123  0uhgrsubgr  39125