Theorem sseq1 3510

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 3504	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3496	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 464	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3496	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 463	. . 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 367   = wceq 1398   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475

This theorem is referenced by:  sseq12  3512  sseq1i  3513  sseq1d  3516  nssne2  3546  psseq1  3577  uneqdifeq  3904  sbss  3927  pwjust  4000  elpw  4005  elpwg  4007  pwpw0  4164  sssn  4174  ssunsn2  4175  pwsnALT  4230  unimax  4270  trss  4541  sseliALT  4570  elssabg  4592  intabs  4598  nnullss  4699  exss  4700  fri  4830  releq  5073  xpsspw  5104  iss  5309  relcnvtr  5510  fununi  5636  ssimaex  5913  isofrlem  6211  onssmin  6605  tfis  6662  tfisi  6666  funcnvuni  6726  ffoss  6734  f1oweALT  6757  frxp  6883  tfrlem1  7037  oawordeu  7196  qsss  7364  boxcutc  7505  sbthlem2  7621  sbth  7630  php  7694  isinf  7726  findcard2d  7754  unbnn2  7769  domunfican  7785  fiint  7789  finsschain  7819  indexfi  7820  dffi3  7883  hartogslem1  7959  cantnfval2  8079  cantnfle  8081  cantnflem1  8099  cantnfval2OLD  8109  cantnfleOLD  8111  cantnflem1OLD  8122  tz9.1  8151  setind  8156  tcvalg  8160  scott0  8295  bnd2  8302  carduni  8353  cardaleph  8461  alephinit  8467  aceq3lem  8492  dfac12lem3  8516  infmap2  8589  cflem  8617  cflm  8621  cflecard  8624  cfeq0  8627  cfsuc  8628  cfflb  8630  cfslb  8637  cfslb2n  8639  coftr  8644  fin23lem13  8703  fin23lem16  8706  fin23lem19  8707  fin23lem29  8712  fin1a2lem13  8783  itunitc  8792  domtriomlem  8813  axdc3lem2  8822  zorn2lem7  8873  zornn0g  8876  fpwwe2lem5  9001  pwfseqlem4a  9028  pwfseqlem4  9029  wunfi  9088  wunex2  9105  wuncval  9109  rankcf  9144  tskuni  9150  axgroth6  9195  axgroth3  9198  axgroth4  9199  fzoss1  11829  fsuppmapnn0fiubex  12083  hashf1lem2  12492  cleq1lem  12903  rtrclreclem4  12979  sumeq1  13596  fsumcvg3  13636  fsum2d  13671  fsumabs  13700  fsumrlim  13710  fsumo1  13711  fsumiun  13720  prodeq1f  13800  fprod2d  13870  vdwmc  14583  restsspw  14924  ismred2  15095  mrcval  15102  mrcuni  15113  acsfn  15151  isssc  15311  drsdirfi  15769  ipodrsima  15997  cntzssv  16568  pmtrfrn  16685  pmtrrn2  16687  pmtrdifellem1  16703  pmtrdifellem2  16704  isslw  16830  sylow2alem2  16840  sylow2a  16841  efgval  16937  gsumzaddlem  17136  gsumzaddlemOLD  17138  ablfac1eulem  17321  lspval  17819  lspindpi  17976  aspval  18175  mplsubglem  18291  mpllsslem  18292  mplsubglemOLD  18293  mpllsslemOLD  18294  mplcoe1  18325  mplcoe5  18329  mplcoe2OLD  18331  znf1o  18766  zntoslem  18771  mdetunilem9  19292  uniopn  19576  fiinopn  19580  fiinbas  19623  baspartn  19625  eltg2  19629  eltg3  19633  topbas  19644  pptbas  19679  clsval  19708  neival  19773  neiint  19775  neips  19784  opnneissb  19785  opnssneib  19786  innei  19796  neiptoptop  19802  neiptopnei  19803  restbas  19829  restcld  19843  neitr  19851  restcls  19852  restntr  19853  cnpdis  19964  nrmsep3  20026  cmpsublem  20069  cmpsub  20070  fiuncmp  20074  uncon  20099  1stcfb  20115  2ndc1stc  20121  1stcrest  20123  2ndcctbss  20125  2ndcomap  20128  dis2ndc  20130  lly1stc  20166  refssex  20181  refun0  20185  llycmpkgen2  20220  txbas  20237  eltx  20238  ptuni2  20246  neitx  20277  ptpjopn  20282  ptcld  20283  txlm  20318  tx1stc  20320  txkgen  20322  xkopt  20325  xkococnlem  20329  ptcmpfi  20483  fbssfi  20507  opnfbas  20512  isfil2  20526  isfildlem  20527  snfil  20534  fsubbas  20537  ssfg  20542  fgss2  20544  fgcl  20548  fbasrn  20554  fgtr  20560  ufli  20584  uffix  20591  rnelfmlem  20622  fclscf  20695  alexsublem  20713  alexsubALTlem2  20717  alexsubALTlem3  20718  alexsubALTlem4  20719  alexsubALT  20720  tmdgsum2  20764  subgntr  20774  opnsubg  20775  qustgpopn  20787  tsmsfbas  20795  tsmsgsum  20806  tsmsgsumOLD  20809  tsmsresOLD  20814  tsmsres  20815  tsmsf1o  20816  tsmsxplem1  20824  tsmsxp  20826  isust  20875  ustssel  20877  ustincl  20879  ustdiag  20880  ustinvel  20881  ustexhalf  20882  ustexsym  20887  ust0  20891  restutop  20909  ustuqtop4  20916  utopsnneiplem  20919  blssexps  21098  blssex  21099  neibl  21173  blcld  21177  met1stc  21193  met2ndci  21194  metrest  21196  prdsxmslem2  21201  metustfbasOLD  21237  metustfbas  21238  cfilucfilOLD  21241  cfilucfil  21242  metuel2  21251  metustblOLD  21252  metustbl  21253  restmetu  21259  dscopn  21263  isngp2  21286  tgioo  21470  tgqioo  21474  zdis  21490  xrge0tsms  21508  fsumcn  21543  ovolval  22054  volivth  22185  vitalilem2  22187  itgfsum  22402  limcun  22468  recnprss  22477  dvmptfsum  22545  ftc1a  22607  plyssc  22766  efopn  23210  jensen  23519  tglnunirn  24139  usgraedgprv  24581  frisusgranb  25202  hhsssh  26386  shintcl  26449  chintcl  26451  spanval  26452  omlsi  26523  pjoml  26555  chnlen0  26563  chsscon3  26619  chlejb1  26631  chnle  26633  spanun  26664  h1datom  26701  cmbr4i  26720  pjoml2  26730  pjoml3  26731  lecm  26736  osumcor2i  26763  osum  26764  spansncv  26772  pjcjt2  26811  pjopyth  26839  hstel2  27339  stj  27355  stcltr1i  27394  mdi  27415  mdbr3  27417  mdbr4  27418  dmdbr  27419  dmdmd  27420  dmdbr5  27428  mdsl1i  27441  mdslmd1lem3  27447  mdslmd1lem4  27448  mdslmd1i  27449  csmdsymi  27454  atss  27466  atom1d  27473  superpos  27474  chcv1  27475  shatomici  27478  shatomistici  27481  hatomistici  27482  chrelat2  27490  chirredi  27514  atcvat4i  27517  mdsymlem2  27524  mdsymlem6  27528  dmdbr6ati  27543  dmdbr7ati  27544  gsumle  28007  gsumvsca1  28011  gsumvsca2  28012  xrge0tsmsd  28013  tpr2rico  28132  issiga  28344  isrnsigaOLD  28345  isrnsiga  28346  sigagenval  28373  measiuns  28428  dya2icoseg  28488  dya2iocnrect  28492  dya2iocuni  28494  carsgmon  28525  carsgsigalem  28526  carsgclctunlem2  28530  carsgclctun  28532  kur14lem1  28917  cvmopnlem  28990  dfon2lem3  29460  dfon2lem7  29464  frmin  29565  wfrlem1  29586  wfrlem4  29589  wfrlem15  29600  frrlem1  29630  frrlem3  29632  brsset  29770  onsucsuccmpi  30139  mblfinlem2  30295  mblfinlem3  30296  mblfinlem4  30297  ismblfin  30298  ovoliunnfl  30299  voliunnfl  30301  volsupnfl  30302  fness  30410  fneref  30411  fnessref  30418  neibastop2lem  30421  topmeet  30425  fnejoin2  30430  tailfb  30438  filnetlem4  30442  indexa  30467  indexdom  30468  neificl  30489  istotbnd3  30510  sstotbnd2  30513  sstotbnd  30514  equivtotbnd  30517  ssbnd  30527  heiborlem1  30550  heiborlem6  30555  heiborlem8  30557  heiborlem10  30559  unichnidl  30671  pridl  30677  ismaxidl  30680  igenval  30701  igenval2  30706  ispridlc  30710  ismrcd1  30873  ismrcd2  30874  ismrc  30876  mzpcompact2lem  30926  aomclem6  31247  hbtlem6  31322  rgspnval  31361  islptre  31867  dvmptconst  31952  dvmptidg  31954  dvmulcncf  31964  dvdivcncf  31966  dvmptfprod  31984  stoweidlem51  32075  stoweidlem52  32076  fourierdlem103  32234  fourierdlem104  32235  onfrALTlem5  33727  onfrALTlem5VD  34105  bnj517  34363  bnj1118  34460  bnj1145  34469  bnj1154  34475  bnj1452  34528  bnj1498  34537  bj-snglss  34948  lsmsat  35149  lssatomic  35152  lssats  35153  lsat0cv  35174  lcvexchlem4  35178  lcvexchlem5  35179  lsatcvatlem  35190  l1cvpat  35195  ispsubsp  35885  linepsubN  35892  pclvalN  36030  ispsubclN  36077  ispsubcl2N  36087  pclfinclN  36090  diaelrnN  37188  docavalN  37266  dochval  37494  dvh4dimat  37581  dochexmidlem1  37603  lpolconN  37630  mapdordlem2  37780  ssficl  38186  ssuncl  38187  ssdifcl  38188  sssymdifcl  38189  iunrelexpmin1  38228  iunrelexpmin2  38229