Theorem sseq1 3626

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 3618	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3610	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 482	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3610	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 481	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( B C_ C -> A C_ C ) )
6	3, 5	impbid 202	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
7	1, 6	sylbi 207	1 |- ( A = B -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sseq12  3628  sseq1i  3629  sseq1d  3632  nssne2  3662  psseq1  3694  uneqdifeq  4057  uneqdifeqOLD  4058  sbss  4084  pwjust  4159  elpw  4164  elpwg  4166  pwpw0  4344  sssn  4358  ssunsn2  4359  pwsnALT  4429  unimax  4473  trss  4761  trssOLD  4762  sseliALT  4791  elssabg  4819  intabs  4825  nnullss  4930  exss  4931  fri  5076  releq  5201  iss  5447  relcnvtr  5655  fununi  5964  ssimaex  6263  isofrlem  6590  onssmin  6997  tfis  7054  tfisi  7058  funcnvuni  7119  ffoss  7127  f1oweALT  7152  frxp  7287  wfrlem1  7414  wfrlem4  7418  wfrlem15  7429  tfrlem1  7472  oawordeu  7635  qsss  7808  boxcutc  7951  sbthlem2  8071  sbth  8080  php  8144  isinf  8173  findcard2d  8202  unbnn2  8217  domunfican  8233  fiint  8237  finsschain  8273  indexfi  8274  dffi3  8337  hartogslem1  8447  cantnfval2  8566  cantnfle  8568  cantnflem1  8586  tz9.1  8605  setind  8610  tcvalg  8614  scott0  8749  bnd2  8756  carduni  8807  cardaleph  8912  alephinit  8918  aceq3lem  8943  dfac12lem3  8967  infmap2  9040  cflem  9068  cflm  9072  cflecard  9075  cfeq0  9078  cfsuc  9079  cfflb  9081  cfslb  9088  cfslb2n  9090  coftr  9095  fin23lem13  9154  fin23lem16  9157  fin23lem19  9158  fin23lem29  9163  fin1a2lem13  9234  itunitc  9243  domtriomlem  9264  axdc3lem2  9273  zorn2lem7  9324  zornn0g  9327  fpwwe2lem5  9456  pwfseqlem4a  9483  pwfseqlem4  9484  wunfi  9543  wunex2  9560  wuncval  9564  rankcf  9599  tskuni  9605  axgroth6  9650  axgroth3  9653  axgroth4  9654  fzoss1  12495  fsuppmapnn0fiubex  12792  hashf1lem2  13240  cleq1lem  13721  rtrclreclem4  13801  sumeq1  14419  fsumcvg3  14460  fsum2d  14502  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  prodeq1f  14638  fprod2d  14711  lcmfunsnlem  15354  coprmprod  15375  vdwmc  15682  prmgaplem3  15757  prmgaplem4  15758  restsspw  16092  ismred2  16263  mrcval  16270  mrcuni  16281  acsfn  16320  isssc  16480  drsdirfi  16938  ipodrsima  17165  cntzssv  17761  pmtrfrn  17878  pmtrrn2  17880  pmtrdifellem1  17896  pmtrdifellem2  17897  isslw  18023  sylow2alem2  18033  sylow2a  18034  efgval  18130  gsumzaddlem  18321  ablfac1eulem  18471  lspval  18975  lspindpi  19132  aspval  19328  mplsubglem  19434  mpllsslem  19435  mplcoe1  19465  mplcoe5  19468  znf1o  19900  zntoslem  19905  mdetunilem9  20426  uniopn  20702  fiinopn  20706  fiinbas  20756  baspartn  20758  eltg2  20762  eltg3  20766  topbas  20776  pptbas  20812  clsval  20841  neival  20906  neiint  20908  neips  20917  opnneissb  20918  opnssneib  20919  innei  20929  neiptoptop  20935  neiptopnei  20936  restbas  20962  restcld  20976  neitr  20984  restcls  20985  restntr  20986  cnpdis  21097  cmpsublem  21202  cmpsub  21203  fiuncmp  21207  unconn  21232  1stcfb  21248  2ndc1stc  21254  1stcrest  21256  2ndcctbss  21258  2ndcomap  21261  dis2ndc  21263  lly1stc  21299  refssex  21314  refun0  21318  llycmpkgen2  21353  txbas  21370  eltx  21371  ptuni2  21379  neitx  21410  ptpjopn  21415  ptcld  21416  txlm  21451  tx1stc  21453  txkgen  21455  xkopt  21458  xkococnlem  21462  ptcmpfi  21616  fbssfi  21641  opnfbas  21646  isfil2  21660  isfildlem  21661  snfil  21668  fsubbas  21671  ssfg  21676  fgss2  21678  fgcl  21682  fbasrn  21688  fgtr  21694  ufli  21718  uffix  21725  rnelfmlem  21756  fclscf  21829  alexsublem  21848  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  tmdgsum2  21900  subgntr  21910  opnsubg  21911  qustgpopn  21923  tsmsfbas  21931  tsmsgsum  21942  tsmsres  21947  tsmsf1o  21948  tsmsxplem1  21956  tsmsxp  21958  isust  22007  ustssel  22009  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ustexsym  22019  ust0  22023  restutop  22041  ustuqtop4  22048  utopsnneiplem  22051  blssexps  22231  blssex  22232  neibl  22306  blcld  22310  met1stc  22326  met2ndci  22327  metrest  22329  prdsxmslem2  22334  metustfbas  22362  cfilucfil  22364  metuel2  22370  metustbl  22371  restmetu  22375  dscopn  22378  isngp2  22401  tgioo  22599  tgqioo  22603  zdis  22619  xrge0tsms  22637  fsumcn  22673  ovolval  23242  volivth  23375  vitalilem2  23378  itgfsum  23593  limcun  23659  recnprss  23668  dvmptfsum  23738  ftc1a  23800  plyssc  23956  efopn  24404  jensen  24715  tglnunirn  25443  lpvtx  25963  umgredgprv  26002  usgredgprvALT  26087  issubgr2  26164  subgrprop2  26166  egrsubgr  26169  0uhgrsubgr  26171  frcond3  27133  hhsssh  28126  shintcl  28189  chintcl  28191  spanval  28192  omlsi  28263  pjoml  28295  chnlen0  28303  chsscon3  28359  chlejb1  28371  chnle  28373  spanun  28404  h1datom  28441  cmbr4i  28460  pjoml2  28470  pjoml3  28471  lecm  28476  osumcor2i  28503  osum  28504  spansncv  28512  pjcjt2  28551  pjopyth  28579  hstel2  29078  stj  29094  stcltr1i  29133  mdi  29154  mdbr3  29156  mdbr4  29157  dmdbr  29158  dmdmd  29159  dmdbr5  29167  mdsl1i  29180  mdslmd1lem3  29186  mdslmd1lem4  29187  mdslmd1i  29188  csmdsymi  29193  atss  29205  atom1d  29212  superpos  29213  chcv1  29214  shatomici  29217  shatomistici  29220  hatomistici  29221  chrelat2  29229  chirredi  29253  atcvat4i  29256  mdsymlem2  29263  mdsymlem6  29267  dmdbr6ati  29282  dmdbr7ati  29283  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  xrge0tsmsd  29785  tpr2rico  29958  issiga  30174  isrnsigaOLD  30175  isrnsiga  30176  sigagenval  30203  measiuns  30280  dya2icoseg  30339  dya2iocnrect  30343  dya2iocuni  30345  carsgmon  30376  carsgsigalem  30377  carsgclctunlem2  30381  carsgclctun  30383  pmeasmono  30386  pmeasadd  30387  bnj517  30955  bnj1118  31052  bnj1145  31061  bnj1154  31067  bnj1452  31120  bnj1498  31129  kur14lem1  31188  cvmopnlem  31260  dfon2lem3  31690  dfon2lem7  31694  frmin  31739  frrlem1  31780  frrlem3  31782  brsslt  31900  brsset  31996  fness  32344  fneref  32345  fnessref  32352  neibastop2lem  32355  topmeet  32359  fnejoin2  32364  tailfb  32372  filnetlem4  32376  onsucsuccmpi  32442  bj-snglss  32958  bj-restpw  33045  dissneqlem  33187  relowlssretop  33211  relowlpssretop  33212  matunitlindflem1  33405  ptrecube  33409  poimirlem29  33438  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  indexa  33528  indexdom  33529  neificl  33549  istotbnd3  33570  sstotbnd2  33573  sstotbnd  33574  equivtotbnd  33577  ssbnd  33587  heiborlem1  33610  heiborlem6  33615  heiborlem8  33617  heiborlem10  33619  unichnidl  33830  pridl  33836  ismaxidl  33839  igenval  33860  igenval2  33865  ispridlc  33869  relcnveq3  34092  iss2  34112  lsmsat  34295  lssatomic  34298  lssats  34299  lsat0cv  34320  lcvexchlem4  34324  lcvexchlem5  34325  lsatcvatlem  34336  l1cvpat  34341  ispsubsp  35031  linepsubN  35038  pclvalN  35176  ispsubclN  35223  ispsubcl2N  35233  pclfinclN  35236  diaelrnN  36334  docavalN  36412  dochval  36640  dvh4dimat  36727  dochexmidlem1  36749  lpolconN  36776  mapdordlem2  36926  ismrcd1  37261  ismrcd2  37262  ismrc  37264  mzpcompact2lem  37314  aomclem6  37629  hbtlem6  37699  rgspnval  37738  ssficl  37874  ssuncl  37875  ssdifcl  37876  sssymdifcl  37877  elmapintrab  37882  clcnvlem  37930  iunrelexpmin1  38000  iunrelexpmin2  38004  clsk3nimkb  38338  clsk1indlem1  38343  isotone1  38346  isotone2  38347  ntrclsiso  38365  gneispace  38432  gneispacess2  38444  onfrALTlem5  38757  onfrALTlem5VD  39121  islptre  39851  dvmptconst  40129  dvmptidg  40131  dvmulcncf  40140  dvdivcncf  40142  dvmptfprod  40160  stoweidlem51  40268  stoweidlem52  40269  fourierdlem103  40426  fourierdlem104  40427  ioorrnopnlem  40524  ioorrnopnxrlem  40526  salgenval  40541  ovnval2  40759  ovncvrrp  40778  ovnsubaddlem1  40784  ovnsubadd  40786  ovncvr2  40825  hspmbl  40843  uspgrsprfo  41756  setrec1lem1  42434  setrec1lem4  42437  setrec2fun  42439  elsetrecslem  42444  elpglem2  42455