Theorem sseq1 3372

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 3366	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3358	. . . 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 3358	. . . 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 1369   C_ wss 3323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337

This theorem is referenced by:  sseq12  3374  sseq1i  3375  sseq1d  3378  nssne2  3408  psseq1  3438  uneqdifeq  3762  sbss  3784  pwjust  3856  elpw  3861  elpwg  3863  pwpw0  4016  sssn  4026  ssunsn2  4027  pwsnALT  4081  unimax  4122  trss  4389  sseliALT  4418  elssabg  4442  intabs  4448  nnullss  4549  exss  4550  fri  4677  releq  4917  xpsspw  4948  iss  5149  relcnvtr  5352  fununi  5479  ssimaex  5751  isofrlem  6026  onssmin  6403  tfis  6460  tfisi  6464  funcnvuni  6525  ffoss  6533  f1oweALT  6556  frxp  6677  tfrlem1  6827  oawordeu  6986  qsss  7153  boxcutc  7298  sbthlem2  7414  sbth  7423  php  7487  isinf  7518  findcard2d  7546  unbnn2  7561  domunfican  7576  fiint  7580  finsschain  7610  indexfi  7611  dffi3  7673  hartogslem1  7748  sucprcregOLD  7807  cantnfval2  7869  cantnfle  7871  cantnflem1  7889  cantnfval2OLD  7899  cantnfleOLD  7901  cantnflem1OLD  7912  tz9.1  7941  setind  7946  tcvalg  7950  scott0  8085  bnd2  8092  carduni  8143  cardaleph  8251  alephinit  8257  aceq3lem  8282  dfac12lem3  8306  infmap2  8379  cflem  8407  cflm  8411  cflecard  8414  cfeq0  8417  cfsuc  8418  cfflb  8420  cfslb  8427  cfslb2n  8429  coftr  8434  fin23lem13  8493  fin23lem16  8496  fin23lem19  8497  fin23lem29  8502  fin1a2lem13  8573  itunitc  8582  domtriomlem  8603  axdc3lem2  8612  zorn2lem7  8663  zornn0g  8666  fpwwe2lem5  8793  pwfseqlem4a  8820  pwfseqlem4  8821  wunfi  8880  wunex2  8897  wuncval  8901  rankcf  8936  tskuni  8942  axgroth6  8987  axgroth3  8990  axgroth4  8991  fzoss1  11568  hashf1lem2  12201  sumeq1  13158  fsumcvg3  13198  fsum2d  13230  fsumabs  13256  fsumrlim  13266  fsumo1  13267  fsumiun  13276  vdwmc  14031  restsspw  14362  ismred2  14533  mrcval  14540  mrcuni  14551  acsfn  14589  isssc  14725  drsdirfi  15100  ipodrsima  15327  cntzssv  15837  pmtrfrn  15955  pmtrrn2  15957  pmtrdifellem1  15973  pmtrdifellem2  15974  isslw  16098  sylow2alem2  16108  sylow2a  16109  efgval  16205  gsumzaddlem  16399  gsumzaddlemOLD  16401  ablfac1eulem  16561  lspval  17033  lspindpi  17190  aspval  17376  mplsubglem  17487  mpllsslem  17488  mplsubglemOLD  17489  mpllsslemOLD  17490  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  znf1o  17959  zntoslem  17964  mdetunilem9  18401  uniopn  18485  fiinopn  18489  fiinbas  18532  baspartn  18534  eltg2  18538  eltg3  18542  topbas  18552  pptbas  18587  clsval  18616  neival  18681  neiint  18683  neips  18692  opnneissb  18693  opnssneib  18694  innei  18704  neiptoptop  18710  neiptopnei  18711  restbas  18737  restcld  18751  neitr  18759  restcls  18760  restntr  18761  cnpdis  18872  nrmsep3  18934  cmpsublem  18977  cmpsub  18978  fiuncmp  18982  uncon  19008  1stcfb  19024  2ndc1stc  19030  1stcrest  19032  2ndcctbss  19034  2ndcomap  19037  dis2ndc  19039  lly1stc  19075  llycmpkgen2  19098  txbas  19115  eltx  19116  ptuni2  19124  neitx  19155  ptpjopn  19160  ptcld  19161  txlm  19196  tx1stc  19198  txkgen  19200  xkopt  19203  xkococnlem  19207  ptcmpfi  19361  fbssfi  19385  opnfbas  19390  isfil2  19404  isfildlem  19405  snfil  19412  fsubbas  19415  ssfg  19420  fgss2  19422  fgcl  19426  fbasrn  19432  fgtr  19438  ufli  19462  uffix  19469  rnelfmlem  19500  fclscf  19573  alexsublem  19591  alexsubALTlem2  19595  alexsubALTlem3  19596  alexsubALTlem4  19597  alexsubALT  19598  tmdgsum2  19642  subgntr  19652  opnsubg  19653  divstgpopn  19665  tsmsfbas  19673  tsmsgsum  19684  tsmsgsumOLD  19687  tsmsresOLD  19692  tsmsres  19693  tsmsf1o  19694  tsmsxplem1  19702  tsmsxp  19704  isust  19753  ustssel  19755  ustincl  19757  ustdiag  19758  ustinvel  19759  ustexhalf  19760  ustexsym  19765  ust0  19769  restutop  19787  ustuqtop4  19794  utopsnneiplem  19797  blssexps  19976  blssex  19977  neibl  20051  blcld  20055  met1stc  20071  met2ndci  20072  metrest  20074  prdsxmslem2  20079  metustfbasOLD  20115  metustfbas  20116  cfilucfilOLD  20119  cfilucfil  20120  metuel2  20129  metustblOLD  20130  metustbl  20131  restmetu  20137  dscopn  20141  isngp2  20164  tgioo  20348  tgqioo  20352  zdis  20368  xrge0tsms  20386  fsumcn  20421  ovolval  20932  volivth  21062  vitalilem2  21064  itgfsum  21279  limcun  21345  recnprss  21354  dvmptfsum  21422  ftc1a  21484  plyssc  21643  efopn  22078  jensen  22357  tglnunirn  22957  usgraedgprv  23246  hhsssh  24621  shintcl  24684  chintcl  24686  spanval  24687  omlsi  24758  pjoml  24790  chnlen0  24798  chsscon3  24854  chlejb1  24866  chnle  24868  spanun  24899  h1datom  24936  cmbr4i  24955  pjoml2  24965  pjoml3  24966  lecm  24971  osumcor2i  24998  osum  24999  spansncv  25007  pjcjt2  25046  pjopyth  25074  hstel2  25574  stj  25590  stcltr1i  25629  mdi  25650  mdbr3  25652  mdbr4  25653  dmdbr  25654  dmdmd  25655  dmdbr5  25663  mdsl1i  25676  mdslmd1lem3  25682  mdslmd1lem4  25683  mdslmd1i  25684  csmdsymi  25689  atss  25701  atom1d  25708  superpos  25709  chcv1  25710  shatomici  25713  shatomistici  25716  hatomistici  25717  chrelat2  25725  chirredi  25749  atcvat4i  25752  mdsymlem2  25759  mdsymlem6  25763  dmdbr6ati  25778  dmdbr7ati  25779  gsumle  26197  gsumvsca1  26202  gsumvsca2  26203  xrge0tsmsd  26204  tpr2rico  26294  issiga  26506  isrnsigaOLD  26507  isrnsiga  26508  sigagenval  26535  measiuns  26583  dya2icoseg  26644  dya2iocnrect  26648  dya2iocuni  26650  kur14lem1  27046  cvmopnlem  27119  rtrclreclem.min  27300  prodeq1f  27372  fprod2d  27443  dfon2lem3  27549  dfon2lem7  27553  frmin  27654  wfrlem1  27675  wfrlem4  27678  wfrlem15  27689  frrlem1  27719  frrlem3  27721  brsset  27871  onsucsuccmpi  28241  mblfinlem2  28382  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  refssex  28506  fness  28507  fneref  28509  fnessref  28518  neibastop2lem  28534  topmeet  28538  fnejoin2  28543  tailfb  28551  filnetlem4  28555  indexa  28580  indexdom  28581  neificl  28602  istotbnd3  28623  sstotbnd2  28626  sstotbnd  28627  equivtotbnd  28630  ssbnd  28640  heiborlem1  28663  heiborlem6  28668  heiborlem8  28670  heiborlem10  28672  unichnidl  28784  pridl  28790  ismaxidl  28793  igenval  28814  igenval2  28819  ispridlc  28823  ismrcd1  28987  ismrcd2  28988  ismrc  28990  mzpcompact2lem  29041  aomclem6  29365  hbtlem6  29438  rgspnval  29478  stoweidlem51  29799  stoweidlem52  29800  frisusgranb  30542  fsuppmapnn0fiubex  30749  onfrALTlem5  31137  onfrALTlem5VD  31508  bnj517  31765  bnj1118  31862  bnj1145  31871  bnj1154  31877  bnj1452  31930  bnj1498  31939  bj-snglss  32310  lsmsat  32493  lssatomic  32496  lssats  32497  lsat0cv  32518  lcvexchlem4  32522  lcvexchlem5  32523  lsatcvatlem  32534  l1cvpat  32539  ispsubsp  33229  linepsubN  33236  pclvalN  33374  ispsubclN  33421  ispsubcl2N  33431  pclfinclN  33434  diaelrnN  34530  docavalN  34608  dochval  34836  dvh4dimat  34923  dochexmidlem1  34945  lpolconN  34972  mapdordlem2  35122