Theorem sseq1 3507

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 3501	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3493	. . . 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 3493	. . . 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 1381   C_ wss 3458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472

This theorem is referenced by:  sseq12  3509  sseq1i  3510  sseq1d  3513  nssne2  3543  psseq1  3573  uneqdifeq  3898  sbss  3920  pwjust  3994  elpw  3999  elpwg  4001  pwpw0  4159  sssn  4169  ssunsn2  4170  pwsnALT  4225  unimax  4266  trss  4535  sseliALT  4564  elssabg  4588  intabs  4594  nnullss  4695  exss  4696  fri  4827  releq  5071  xpsspw  5102  iss  5307  relcnvtr  5513  fununi  5640  ssimaex  5919  isofrlem  6217  onssmin  6613  tfis  6670  tfisi  6674  funcnvuni  6734  ffoss  6742  f1oweALT  6765  frxp  6891  tfrlem1  7043  oawordeu  7202  qsss  7370  boxcutc  7510  sbthlem2  7626  sbth  7635  php  7699  isinf  7731  findcard2d  7760  unbnn2  7775  domunfican  7791  fiint  7795  finsschain  7825  indexfi  7826  dffi3  7889  hartogslem1  7965  sucprcregOLD  8024  cantnfval2  8086  cantnfle  8088  cantnflem1  8106  cantnfval2OLD  8116  cantnfleOLD  8118  cantnflem1OLD  8129  tz9.1  8158  setind  8163  tcvalg  8167  scott0  8302  bnd2  8309  carduni  8360  cardaleph  8468  alephinit  8474  aceq3lem  8499  dfac12lem3  8523  infmap2  8596  cflem  8624  cflm  8628  cflecard  8631  cfeq0  8634  cfsuc  8635  cfflb  8637  cfslb  8644  cfslb2n  8646  coftr  8651  fin23lem13  8710  fin23lem16  8713  fin23lem19  8714  fin23lem29  8719  fin1a2lem13  8790  itunitc  8799  domtriomlem  8820  axdc3lem2  8829  zorn2lem7  8880  zornn0g  8883  fpwwe2lem5  9010  pwfseqlem4a  9037  pwfseqlem4  9038  wunfi  9097  wunex2  9114  wuncval  9118  rankcf  9153  tskuni  9159  axgroth6  9204  axgroth3  9207  axgroth4  9208  fzoss1  11826  fsuppmapnn0fiubex  12072  hashf1lem2  12479  sumeq1  13485  fsumcvg3  13525  fsum2d  13560  fsumabs  13589  fsumrlim  13599  fsumo1  13600  fsumiun  13609  vdwmc  14368  restsspw  14701  ismred2  14872  mrcval  14879  mrcuni  14890  acsfn  14928  isssc  15061  drsdirfi  15436  ipodrsima  15664  cntzssv  16235  pmtrfrn  16352  pmtrrn2  16354  pmtrdifellem1  16370  pmtrdifellem2  16371  isslw  16497  sylow2alem2  16507  sylow2a  16508  efgval  16604  gsumzaddlem  16803  gsumzaddlemOLD  16805  ablfac1eulem  16991  lspval  17489  lspindpi  17646  aspval  17845  mplsubglem  17961  mpllsslem  17962  mplsubglemOLD  17963  mpllsslemOLD  17964  mplcoe1  17995  mplcoe5  17999  mplcoe2OLD  18001  znf1o  18457  zntoslem  18462  mdetunilem9  18989  uniopn  19273  fiinopn  19277  fiinbas  19320  baspartn  19322  eltg2  19326  eltg3  19330  topbas  19340  pptbas  19375  clsval  19404  neival  19469  neiint  19471  neips  19480  opnneissb  19481  opnssneib  19482  innei  19492  neiptoptop  19498  neiptopnei  19499  restbas  19525  restcld  19539  neitr  19547  restcls  19548  restntr  19549  cnpdis  19660  nrmsep3  19722  cmpsublem  19765  cmpsub  19766  fiuncmp  19770  uncon  19796  1stcfb  19812  2ndc1stc  19818  1stcrest  19820  2ndcctbss  19822  2ndcomap  19825  dis2ndc  19827  lly1stc  19863  refssex  19878  refun0  19882  llycmpkgen2  19917  txbas  19934  eltx  19935  ptuni2  19943  neitx  19974  ptpjopn  19979  ptcld  19980  txlm  20015  tx1stc  20017  txkgen  20019  xkopt  20022  xkococnlem  20026  ptcmpfi  20180  fbssfi  20204  opnfbas  20209  isfil2  20223  isfildlem  20224  snfil  20231  fsubbas  20234  ssfg  20239  fgss2  20241  fgcl  20245  fbasrn  20251  fgtr  20257  ufli  20281  uffix  20288  rnelfmlem  20319  fclscf  20392  alexsublem  20410  alexsubALTlem2  20414  alexsubALTlem3  20415  alexsubALTlem4  20416  alexsubALT  20417  tmdgsum2  20461  subgntr  20471  opnsubg  20472  qustgpopn  20484  tsmsfbas  20492  tsmsgsum  20503  tsmsgsumOLD  20506  tsmsresOLD  20511  tsmsres  20512  tsmsf1o  20513  tsmsxplem1  20521  tsmsxp  20523  isust  20572  ustssel  20574  ustincl  20576  ustdiag  20577  ustinvel  20578  ustexhalf  20579  ustexsym  20584  ust0  20588  restutop  20606  ustuqtop4  20613  utopsnneiplem  20616  blssexps  20795  blssex  20796  neibl  20870  blcld  20874  met1stc  20890  met2ndci  20891  metrest  20893  prdsxmslem2  20898  metustfbasOLD  20934  metustfbas  20935  cfilucfilOLD  20938  cfilucfil  20939  metuel2  20948  metustblOLD  20949  metustbl  20950  restmetu  20956  dscopn  20960  isngp2  20983  tgioo  21167  tgqioo  21171  zdis  21187  xrge0tsms  21205  fsumcn  21240  ovolval  21751  volivth  21882  vitalilem2  21884  itgfsum  22099  limcun  22165  recnprss  22174  dvmptfsum  22242  ftc1a  22304  plyssc  22463  efopn  22904  jensen  23183  tglnunirn  23800  usgraedgprv  24241  frisusgranb  24862  hhsssh  26050  shintcl  26113  chintcl  26115  spanval  26116  omlsi  26187  pjoml  26219  chnlen0  26227  chsscon3  26283  chlejb1  26295  chnle  26297  spanun  26328  h1datom  26365  cmbr4i  26384  pjoml2  26394  pjoml3  26395  lecm  26400  osumcor2i  26427  osum  26428  spansncv  26436  pjcjt2  26475  pjopyth  26503  hstel2  27003  stj  27019  stcltr1i  27058  mdi  27079  mdbr3  27081  mdbr4  27082  dmdbr  27083  dmdmd  27084  dmdbr5  27092  mdsl1i  27105  mdslmd1lem3  27111  mdslmd1lem4  27112  mdslmd1i  27113  csmdsymi  27118  atss  27130  atom1d  27137  superpos  27138  chcv1  27139  shatomici  27142  shatomistici  27145  hatomistici  27146  chrelat2  27154  chirredi  27178  atcvat4i  27181  mdsymlem2  27188  mdsymlem6  27192  dmdbr6ati  27207  dmdbr7ati  27208  gsumle  27636  gsumvsca1  27639  gsumvsca2  27640  xrge0tsmsd  27641  tpr2rico  27760  issiga  27977  isrnsigaOLD  27978  isrnsiga  27979  sigagenval  28006  measiuns  28054  dya2icoseg  28114  dya2iocnrect  28118  dya2iocuni  28120  kur14lem1  28516  cvmopnlem  28589  rtrclreclem.min  28936  prodeq1f  29008  fprod2d  29079  dfon2lem3  29185  dfon2lem7  29189  frmin  29290  wfrlem1  29311  wfrlem4  29314  wfrlem15  29325  frrlem1  29355  frrlem3  29357  brsset  29507  onsucsuccmpi  29876  mblfinlem2  30020  mblfinlem3  30021  mblfinlem4  30022  ismblfin  30023  ovoliunnfl  30024  voliunnfl  30026  volsupnfl  30027  fness  30135  fneref  30136  fnessref  30143  neibastop2lem  30146  topmeet  30150  fnejoin2  30155  tailfb  30163  filnetlem4  30167  indexa  30192  indexdom  30193  neificl  30214  istotbnd3  30235  sstotbnd2  30238  sstotbnd  30239  equivtotbnd  30242  ssbnd  30252  heiborlem1  30275  heiborlem6  30280  heiborlem8  30282  heiborlem10  30284  unichnidl  30396  pridl  30402  ismaxidl  30405  igenval  30426  igenval2  30431  ispridlc  30435  ismrcd1  30598  ismrcd2  30599  ismrc  30601  mzpcompact2lem  30652  aomclem6  30973  hbtlem6  31046  rgspnval  31086  islptre  31529  dvmptconst  31610  dvmptidg  31612  dvmulcncf  31622  dvdivcncf  31624  stoweidlem51  31718  stoweidlem52  31719  fourierdlem103  31877  fourierdlem104  31878  onfrALTlem5  33022  onfrALTlem5VD  33393  bnj517  33650  bnj1118  33747  bnj1145  33756  bnj1154  33762  bnj1452  33815  bnj1498  33824  bj-snglss  34240  lsmsat  34435  lssatomic  34438  lssats  34439  lsat0cv  34460  lcvexchlem4  34464  lcvexchlem5  34465  lsatcvatlem  34476  l1cvpat  34481  ispsubsp  35171  linepsubN  35178  pclvalN  35316  ispsubclN  35363  ispsubcl2N  35373  pclfinclN  35376  diaelrnN  36474  docavalN  36552  dochval  36780  dvh4dimat  36867  dochexmidlem1  36889  lpolconN  36916  mapdordlem2  37066  ssficl  37419  ssuncl  37420  ssdifcl  37421  sssymdifcl  37422