Theorem sseq1 3525

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 3519	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3511	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 466	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3511	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 465	. . 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 1379   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  sseq12  3527  sseq1i  3528  sseq1d  3531  nssne2  3561  psseq1  3591  uneqdifeq  3915  sbss  3937  pwjust  4011  elpw  4016  elpwg  4018  pwpw0  4175  sssn  4185  ssunsn2  4186  pwsnALT  4240  unimax  4281  trss  4549  sseliALT  4578  elssabg  4602  intabs  4608  nnullss  4709  exss  4710  fri  4841  releq  5083  xpsspw  5114  iss  5319  relcnvtr  5525  fununi  5652  ssimaex  5930  isofrlem  6222  onssmin  6610  tfis  6667  tfisi  6671  funcnvuni  6734  ffoss  6742  f1oweALT  6765  frxp  6890  tfrlem1  7042  oawordeu  7201  qsss  7369  boxcutc  7509  sbthlem2  7625  sbth  7634  php  7698  isinf  7730  findcard2d  7758  unbnn2  7773  domunfican  7789  fiint  7793  finsschain  7823  indexfi  7824  dffi3  7887  hartogslem1  7963  sucprcregOLD  8022  cantnfval2  8084  cantnfle  8086  cantnflem1  8104  cantnfval2OLD  8114  cantnfleOLD  8116  cantnflem1OLD  8127  tz9.1  8156  setind  8161  tcvalg  8165  scott0  8300  bnd2  8307  carduni  8358  cardaleph  8466  alephinit  8472  aceq3lem  8497  dfac12lem3  8521  infmap2  8594  cflem  8622  cflm  8626  cflecard  8629  cfeq0  8632  cfsuc  8633  cfflb  8635  cfslb  8642  cfslb2n  8644  coftr  8649  fin23lem13  8708  fin23lem16  8711  fin23lem19  8712  fin23lem29  8717  fin1a2lem13  8788  itunitc  8797  domtriomlem  8818  axdc3lem2  8827  zorn2lem7  8878  zornn0g  8881  fpwwe2lem5  9008  pwfseqlem4a  9035  pwfseqlem4  9036  wunfi  9095  wunex2  9112  wuncval  9116  rankcf  9151  tskuni  9157  axgroth6  9202  axgroth3  9205  axgroth4  9206  fzoss1  11816  fsuppmapnn0fiubex  12062  hashf1lem2  12467  sumeq1  13470  fsumcvg3  13510  fsum2d  13545  fsumabs  13574  fsumrlim  13584  fsumo1  13585  fsumiun  13594  vdwmc  14351  restsspw  14683  ismred2  14854  mrcval  14861  mrcuni  14872  acsfn  14910  isssc  15046  drsdirfi  15421  ipodrsima  15648  cntzssv  16161  pmtrfrn  16279  pmtrrn2  16281  pmtrdifellem1  16297  pmtrdifellem2  16298  isslw  16424  sylow2alem2  16434  sylow2a  16435  efgval  16531  gsumzaddlem  16725  gsumzaddlemOLD  16727  ablfac1eulem  16913  lspval  17404  lspindpi  17561  aspval  17748  mplsubglem  17864  mpllsslem  17865  mplsubglemOLD  17866  mpllsslemOLD  17867  mplcoe1  17898  mplcoe5  17902  mplcoe2OLD  17904  znf1o  18357  zntoslem  18362  mdetunilem9  18889  uniopn  19173  fiinopn  19177  fiinbas  19220  baspartn  19222  eltg2  19226  eltg3  19230  topbas  19240  pptbas  19275  clsval  19304  neival  19369  neiint  19371  neips  19380  opnneissb  19381  opnssneib  19382  innei  19392  neiptoptop  19398  neiptopnei  19399  restbas  19425  restcld  19439  neitr  19447  restcls  19448  restntr  19449  cnpdis  19560  nrmsep3  19622  cmpsublem  19665  cmpsub  19666  fiuncmp  19670  uncon  19696  1stcfb  19712  2ndc1stc  19718  1stcrest  19720  2ndcctbss  19722  2ndcomap  19725  dis2ndc  19727  lly1stc  19763  llycmpkgen2  19786  txbas  19803  eltx  19804  ptuni2  19812  neitx  19843  ptpjopn  19848  ptcld  19849  txlm  19884  tx1stc  19886  txkgen  19888  xkopt  19891  xkococnlem  19895  ptcmpfi  20049  fbssfi  20073  opnfbas  20078  isfil2  20092  isfildlem  20093  snfil  20100  fsubbas  20103  ssfg  20108  fgss2  20110  fgcl  20114  fbasrn  20120  fgtr  20126  ufli  20150  uffix  20157  rnelfmlem  20188  fclscf  20261  alexsublem  20279  alexsubALTlem2  20283  alexsubALTlem3  20284  alexsubALTlem4  20285  alexsubALT  20286  tmdgsum2  20330  subgntr  20340  opnsubg  20341  divstgpopn  20353  tsmsfbas  20361  tsmsgsum  20372  tsmsgsumOLD  20375  tsmsresOLD  20380  tsmsres  20381  tsmsf1o  20382  tsmsxplem1  20390  tsmsxp  20392  isust  20441  ustssel  20443  ustincl  20445  ustdiag  20446  ustinvel  20447  ustexhalf  20448  ustexsym  20453  ust0  20457  restutop  20475  ustuqtop4  20482  utopsnneiplem  20485  blssexps  20664  blssex  20665  neibl  20739  blcld  20743  met1stc  20759  met2ndci  20760  metrest  20762  prdsxmslem2  20767  metustfbasOLD  20803  metustfbas  20804  cfilucfilOLD  20807  cfilucfil  20808  metuel2  20817  metustblOLD  20818  metustbl  20819  restmetu  20825  dscopn  20829  isngp2  20852  tgioo  21036  tgqioo  21040  zdis  21056  xrge0tsms  21074  fsumcn  21109  ovolval  21620  volivth  21751  vitalilem2  21753  itgfsum  21968  limcun  22034  recnprss  22043  dvmptfsum  22111  ftc1a  22173  plyssc  22332  efopn  22767  jensen  23046  tglnunirn  23663  usgraedgprv  24052  frisusgranb  24673  hhsssh  25861  shintcl  25924  chintcl  25926  spanval  25927  omlsi  25998  pjoml  26030  chnlen0  26038  chsscon3  26094  chlejb1  26106  chnle  26108  spanun  26139  h1datom  26176  cmbr4i  26195  pjoml2  26205  pjoml3  26206  lecm  26211  osumcor2i  26238  osum  26239  spansncv  26247  pjcjt2  26286  pjopyth  26314  hstel2  26814  stj  26830  stcltr1i  26869  mdi  26890  mdbr3  26892  mdbr4  26893  dmdbr  26894  dmdmd  26895  dmdbr5  26903  mdsl1i  26916  mdslmd1lem3  26922  mdslmd1lem4  26923  mdslmd1i  26924  csmdsymi  26929  atss  26941  atom1d  26948  superpos  26949  chcv1  26950  shatomici  26953  shatomistici  26956  hatomistici  26957  chrelat2  26965  chirredi  26989  atcvat4i  26992  mdsymlem2  26999  mdsymlem6  27003  dmdbr6ati  27018  dmdbr7ati  27019  gsumle  27433  gsumvsca1  27436  gsumvsca2  27437  xrge0tsmsd  27438  tpr2rico  27530  issiga  27751  isrnsigaOLD  27752  isrnsiga  27753  sigagenval  27780  measiuns  27828  dya2icoseg  27888  dya2iocnrect  27892  dya2iocuni  27894  kur14lem1  28290  cvmopnlem  28363  rtrclreclem.min  28545  prodeq1f  28617  fprod2d  28688  dfon2lem3  28794  dfon2lem7  28798  frmin  28899  wfrlem1  28920  wfrlem4  28923  wfrlem15  28934  frrlem1  28964  frrlem3  28966  brsset  29116  onsucsuccmpi  29485  mblfinlem2  29629  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  ovoliunnfl  29633  voliunnfl  29635  volsupnfl  29636  refssex  29753  fness  29754  fneref  29756  fnessref  29765  neibastop2lem  29781  topmeet  29785  fnejoin2  29790  tailfb  29798  filnetlem4  29802  indexa  29827  indexdom  29828  neificl  29849  istotbnd3  29870  sstotbnd2  29873  sstotbnd  29874  equivtotbnd  29877  ssbnd  29887  heiborlem1  29910  heiborlem6  29915  heiborlem8  29917  heiborlem10  29919  unichnidl  30031  pridl  30037  ismaxidl  30040  igenval  30061  igenval2  30066  ispridlc  30070  ismrcd1  30234  ismrcd2  30235  ismrc  30237  mzpcompact2lem  30288  aomclem6  30609  hbtlem6  30682  rgspnval  30722  islptre  31161  dvmptconst  31243  dvmptidg  31245  dvmulcncf  31255  dvdivcncf  31257  stoweidlem51  31351  stoweidlem52  31352  fourierdlem103  31510  fourierdlem104  31511  onfrALTlem5  32394  onfrALTlem5VD  32765  bnj517  33022  bnj1118  33119  bnj1145  33128  bnj1154  33134  bnj1452  33187  bnj1498  33196  bj-snglss  33609  lsmsat  33805  lssatomic  33808  lssats  33809  lsat0cv  33830  lcvexchlem4  33834  lcvexchlem5  33835  lsatcvatlem  33846  l1cvpat  33851  ispsubsp  34541  linepsubN  34548  pclvalN  34686  ispsubclN  34733  ispsubcl2N  34743  pclfinclN  34746  diaelrnN  35842  docavalN  35920  dochval  36148  dvh4dimat  36235  dochexmidlem1  36257  lpolconN  36284  mapdordlem2  36434  ssficl  36774  ssuncl  36775  ssdifcl  36776  sssymdifcl  36777