Theorem sseq1 3486

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 3480	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3472	. . . 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 3472	. . . 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 1370   C_ wss 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3444  df-ss 3451

This theorem is referenced by:  sseq12  3488  sseq1i  3489  sseq1d  3492  nssne2  3522  psseq1  3552  uneqdifeq  3876  sbss  3898  pwjust  3970  elpw  3975  elpwg  3977  pwpw0  4130  sssn  4140  ssunsn2  4141  pwsnALT  4195  unimax  4236  trss  4503  sseliALT  4532  elssabg  4556  intabs  4562  nnullss  4663  exss  4664  fri  4791  releq  5031  xpsspw  5062  iss  5263  relcnvtr  5466  fununi  5593  ssimaex  5866  isofrlem  6141  onssmin  6519  tfis  6576  tfisi  6580  funcnvuni  6641  ffoss  6649  f1oweALT  6672  frxp  6793  tfrlem1  6946  oawordeu  7105  qsss  7272  boxcutc  7417  sbthlem2  7533  sbth  7542  php  7606  isinf  7638  findcard2d  7666  unbnn2  7681  domunfican  7696  fiint  7700  finsschain  7730  indexfi  7731  dffi3  7793  hartogslem1  7868  sucprcregOLD  7927  cantnfval2  7989  cantnfle  7991  cantnflem1  8009  cantnfval2OLD  8019  cantnfleOLD  8021  cantnflem1OLD  8032  tz9.1  8061  setind  8066  tcvalg  8070  scott0  8205  bnd2  8212  carduni  8263  cardaleph  8371  alephinit  8377  aceq3lem  8402  dfac12lem3  8426  infmap2  8499  cflem  8527  cflm  8531  cflecard  8534  cfeq0  8537  cfsuc  8538  cfflb  8540  cfslb  8547  cfslb2n  8549  coftr  8554  fin23lem13  8613  fin23lem16  8616  fin23lem19  8617  fin23lem29  8622  fin1a2lem13  8693  itunitc  8702  domtriomlem  8723  axdc3lem2  8732  zorn2lem7  8783  zornn0g  8786  fpwwe2lem5  8913  pwfseqlem4a  8940  pwfseqlem4  8941  wunfi  9000  wunex2  9017  wuncval  9021  rankcf  9056  tskuni  9062  axgroth6  9107  axgroth3  9110  axgroth4  9111  fzoss1  11694  hashf1lem2  12328  sumeq1  13285  fsumcvg3  13325  fsum2d  13357  fsumabs  13383  fsumrlim  13393  fsumo1  13394  fsumiun  13403  vdwmc  14158  restsspw  14490  ismred2  14661  mrcval  14668  mrcuni  14679  acsfn  14717  isssc  14853  drsdirfi  15228  ipodrsima  15455  cntzssv  15966  pmtrfrn  16084  pmtrrn2  16086  pmtrdifellem1  16102  pmtrdifellem2  16103  isslw  16229  sylow2alem2  16239  sylow2a  16240  efgval  16336  gsumzaddlem  16530  gsumzaddlemOLD  16532  ablfac1eulem  16696  lspval  17180  lspindpi  17337  aspval  17523  mplsubglem  17635  mpllsslem  17636  mplsubglemOLD  17637  mpllsslemOLD  17638  mplcoe1  17669  mplcoe5  17673  mplcoe2OLD  17675  znf1o  18110  zntoslem  18115  mdetunilem9  18559  uniopn  18643  fiinopn  18647  fiinbas  18690  baspartn  18692  eltg2  18696  eltg3  18700  topbas  18710  pptbas  18745  clsval  18774  neival  18839  neiint  18841  neips  18850  opnneissb  18851  opnssneib  18852  innei  18862  neiptoptop  18868  neiptopnei  18869  restbas  18895  restcld  18909  neitr  18917  restcls  18918  restntr  18919  cnpdis  19030  nrmsep3  19092  cmpsublem  19135  cmpsub  19136  fiuncmp  19140  uncon  19166  1stcfb  19182  2ndc1stc  19188  1stcrest  19190  2ndcctbss  19192  2ndcomap  19195  dis2ndc  19197  lly1stc  19233  llycmpkgen2  19256  txbas  19273  eltx  19274  ptuni2  19282  neitx  19313  ptpjopn  19318  ptcld  19319  txlm  19354  tx1stc  19356  txkgen  19358  xkopt  19361  xkococnlem  19365  ptcmpfi  19519  fbssfi  19543  opnfbas  19548  isfil2  19562  isfildlem  19563  snfil  19570  fsubbas  19573  ssfg  19578  fgss2  19580  fgcl  19584  fbasrn  19590  fgtr  19596  ufli  19620  uffix  19627  rnelfmlem  19658  fclscf  19731  alexsublem  19749  alexsubALTlem2  19753  alexsubALTlem3  19754  alexsubALTlem4  19755  alexsubALT  19756  tmdgsum2  19800  subgntr  19810  opnsubg  19811  divstgpopn  19823  tsmsfbas  19831  tsmsgsum  19842  tsmsgsumOLD  19845  tsmsresOLD  19850  tsmsres  19851  tsmsf1o  19852  tsmsxplem1  19860  tsmsxp  19862  isust  19911  ustssel  19913  ustincl  19915  ustdiag  19916  ustinvel  19917  ustexhalf  19918  ustexsym  19923  ust0  19927  restutop  19945  ustuqtop4  19952  utopsnneiplem  19955  blssexps  20134  blssex  20135  neibl  20209  blcld  20213  met1stc  20229  met2ndci  20230  metrest  20232  prdsxmslem2  20237  metustfbasOLD  20273  metustfbas  20274  cfilucfilOLD  20277  cfilucfil  20278  metuel2  20287  metustblOLD  20288  metustbl  20289  restmetu  20295  dscopn  20299  isngp2  20322  tgioo  20506  tgqioo  20510  zdis  20526  xrge0tsms  20544  fsumcn  20579  ovolval  21090  volivth  21221  vitalilem2  21223  itgfsum  21438  limcun  21504  recnprss  21513  dvmptfsum  21581  ftc1a  21643  plyssc  21802  efopn  22237  jensen  22516  tglnunirn  23119  usgraedgprv  23448  hhsssh  24823  shintcl  24886  chintcl  24888  spanval  24889  omlsi  24960  pjoml  24992  chnlen0  25000  chsscon3  25056  chlejb1  25068  chnle  25070  spanun  25101  h1datom  25138  cmbr4i  25157  pjoml2  25167  pjoml3  25168  lecm  25173  osumcor2i  25200  osum  25201  spansncv  25209  pjcjt2  25248  pjopyth  25276  hstel2  25776  stj  25792  stcltr1i  25831  mdi  25852  mdbr3  25854  mdbr4  25855  dmdbr  25856  dmdmd  25857  dmdbr5  25865  mdsl1i  25878  mdslmd1lem3  25884  mdslmd1lem4  25885  mdslmd1i  25886  csmdsymi  25891  atss  25903  atom1d  25910  superpos  25911  chcv1  25912  shatomici  25915  shatomistici  25918  hatomistici  25919  chrelat2  25927  chirredi  25951  atcvat4i  25954  mdsymlem2  25961  mdsymlem6  25965  dmdbr6ati  25980  dmdbr7ati  25981  gsumle  26392  gsumvsca1  26397  gsumvsca2  26398  xrge0tsmsd  26399  tpr2rico  26488  issiga  26700  isrnsigaOLD  26701  isrnsiga  26702  sigagenval  26729  measiuns  26777  dya2icoseg  26837  dya2iocnrect  26841  dya2iocuni  26843  kur14lem1  27239  cvmopnlem  27312  rtrclreclem.min  27494  prodeq1f  27566  fprod2d  27637  dfon2lem3  27743  dfon2lem7  27747  frmin  27848  wfrlem1  27869  wfrlem4  27872  wfrlem15  27883  frrlem1  27913  frrlem3  27915  brsset  28065  onsucsuccmpi  28434  mblfinlem2  28578  mblfinlem3  28579  mblfinlem4  28580  ismblfin  28581  ovoliunnfl  28582  voliunnfl  28584  volsupnfl  28585  refssex  28702  fness  28703  fneref  28705  fnessref  28714  neibastop2lem  28730  topmeet  28734  fnejoin2  28739  tailfb  28747  filnetlem4  28751  indexa  28776  indexdom  28777  neificl  28798  istotbnd3  28819  sstotbnd2  28822  sstotbnd  28823  equivtotbnd  28826  ssbnd  28836  heiborlem1  28859  heiborlem6  28864  heiborlem8  28866  heiborlem10  28868  unichnidl  28980  pridl  28986  ismaxidl  28989  igenval  29010  igenval2  29015  ispridlc  29019  ismrcd1  29183  ismrcd2  29184  ismrc  29186  mzpcompact2lem  29237  aomclem6  29561  hbtlem6  29634  rgspnval  29674  stoweidlem51  29995  stoweidlem52  29996  frisusgranb  30738  fsuppmapnn0fiubex  30949  onfrALTlem5  31583  onfrALTlem5VD  31954  bnj517  32211  bnj1118  32308  bnj1145  32317  bnj1154  32323  bnj1452  32376  bnj1498  32385  bj-snglss  32796  lsmsat  32992  lssatomic  32995  lssats  32996  lsat0cv  33017  lcvexchlem4  33021  lcvexchlem5  33022  lsatcvatlem  33033  l1cvpat  33038  ispsubsp  33728  linepsubN  33735  pclvalN  33873  ispsubclN  33920  ispsubcl2N  33930  pclfinclN  33933  diaelrnN  35029  docavalN  35107  dochval  35335  dvh4dimat  35422  dochexmidlem1  35444  lpolconN  35471  mapdordlem2  35621