Theorem sseq1 3421

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 3415	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3407	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 472	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3407	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 471	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( B C_ C -> A C_ C ) )
6	3, 5	impbid 195	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
7	1, 6	sylbi 200	1 |- ( A = B -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1448   C_ wss 3372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-in 3379  df-ss 3386

This theorem is referenced by:  sseq12  3423  sseq1i  3424  sseq1d  3427  nssne2  3457  psseq1  3488  uneqdifeq  3824  sbss  3847  pwjust  3920  elpw  3925  elpwg  3927  pwpw0  4089  sssn  4099  ssunsn2  4100  pwsnALT  4163  unimax  4203  trss  4478  sseliALT  4508  elssabg  4531  intabs  4537  nnullss  4635  exss  4636  fri  4774  releq  4895  iss  5130  relcnvtr  5334  fununi  5631  ssimaex  5914  isofrlem  6217  onssmin  6612  tfis  6669  tfisi  6673  funcnvuni  6734  ffoss  6742  f1oweALT  6765  frxp  6894  wfrlem1  7022  wfrlem4  7026  wfrlem15  7037  tfrlem1  7081  oawordeu  7243  qsss  7411  boxcutc  7552  sbthlem2  7670  sbth  7679  php  7743  isinf  7772  findcard2d  7800  unbnn2  7815  domunfican  7831  fiint  7835  finsschain  7868  indexfi  7869  dffi3  7932  hartogslem1  8044  cantnfval2  8161  cantnfle  8163  cantnflem1  8181  tz9.1  8200  setind  8205  tcvalg  8209  scott0  8344  bnd2  8351  carduni  8402  cardaleph  8507  alephinit  8513  aceq3lem  8538  dfac12lem3  8562  infmap2  8635  cflem  8663  cflm  8667  cflecard  8670  cfeq0  8673  cfsuc  8674  cfflb  8676  cfslb  8683  cfslb2n  8685  coftr  8690  fin23lem13  8749  fin23lem16  8752  fin23lem19  8753  fin23lem29  8758  fin1a2lem13  8829  itunitc  8838  domtriomlem  8859  axdc3lem2  8868  zorn2lem7  8919  zornn0g  8922  fpwwe2lem5  9046  pwfseqlem4a  9073  pwfseqlem4  9074  wunfi  9133  wunex2  9150  wuncval  9154  rankcf  9189  tskuni  9195  axgroth6  9240  axgroth3  9243  axgroth4  9244  fzoss1  11938  fsuppmapnn0fiubex  12198  hashf1lem2  12614  cleq1lem  13057  rtrclreclem4  13135  sumeq1  13766  fsumcvg3  13806  fsum2d  13843  fsumabs  13872  fsumrlim  13882  fsumo1  13883  fsumiun  13892  prodeq1f  13973  fprod2d  14046  lcmfunsnlem  14625  coprmprod  14689  vdwmc  14939  prmgaplem3  15034  prmgaplem4  15035  restsspw  15341  ismred2  15520  mrcval  15527  mrcuni  15538  acsfn  15576  isssc  15736  drsdirfi  16194  ipodrsima  16422  cntzssv  16993  pmtrfrn  17110  pmtrrn2  17112  pmtrdifellem1  17128  pmtrdifellem2  17129  isslw  17271  sylow2alem2  17281  sylow2a  17282  efgval  17378  gsumzaddlem  17565  ablfac1eulem  17716  lspval  18209  lspindpi  18366  aspval  18563  mplsubglem  18669  mpllsslem  18670  mplcoe1  18700  mplcoe5  18703  znf1o  19133  zntoslem  19138  mdetunilem9  19656  uniopn  19938  fiinopn  19942  fiinbas  19978  baspartn  19980  eltg2  19984  eltg3  19988  topbas  19999  pptbas  20034  clsval  20063  neival  20129  neiint  20131  neips  20140  opnneissb  20141  opnssneib  20142  innei  20152  neiptoptop  20158  neiptopnei  20159  restbas  20185  restcld  20199  neitr  20207  restcls  20208  restntr  20209  cnpdis  20320  nrmsep3  20382  cmpsublem  20425  cmpsub  20426  fiuncmp  20430  uncon  20455  1stcfb  20471  2ndc1stc  20477  1stcrest  20479  2ndcctbss  20481  2ndcomap  20484  dis2ndc  20486  lly1stc  20522  refssex  20537  refun0  20541  llycmpkgen2  20576  txbas  20593  eltx  20594  ptuni2  20602  neitx  20633  ptpjopn  20638  ptcld  20639  txlm  20674  tx1stc  20676  txkgen  20678  xkopt  20681  xkococnlem  20685  ptcmpfi  20839  fbssfi  20863  opnfbas  20868  isfil2  20882  isfildlem  20883  snfil  20890  fsubbas  20893  ssfg  20898  fgss2  20900  fgcl  20904  fbasrn  20910  fgtr  20916  ufli  20940  uffix  20947  rnelfmlem  20978  fclscf  21051  alexsublem  21070  alexsubALTlem2  21074  alexsubALTlem3  21075  alexsubALTlem4  21076  alexsubALT  21077  tmdgsum2  21122  subgntr  21132  opnsubg  21133  qustgpopn  21145  tsmsfbas  21153  tsmsgsum  21164  tsmsres  21169  tsmsf1o  21170  tsmsxplem1  21178  tsmsxp  21180  isust  21229  ustssel  21231  ustincl  21233  ustdiag  21234  ustinvel  21235  ustexhalf  21236  ustexsym  21241  ust0  21245  restutop  21263  ustuqtop4  21270  utopsnneiplem  21273  blssexps  21452  blssex  21453  neibl  21527  blcld  21531  met1stc  21547  met2ndci  21548  metrest  21550  prdsxmslem2  21555  metustfbas  21583  cfilucfil  21585  metuel2  21591  metustbl  21592  restmetu  21596  dscopn  21599  isngp2  21622  tgioo  21825  tgqioo  21829  zdis  21845  xrge0tsms  21863  fsumcn  21913  ovolval  22437  ovolvalOLD  22438  volivth  22577  vitalilem2  22579  itgfsum  22796  limcun  22862  recnprss  22871  dvmptfsum  22939  ftc1a  23001  plyssc  23166  efopn  23615  jensen  23926  tglnunirn  24605  usgraedgprv  25115  frisusgranb  25737  hhsssh  26932  shintcl  26995  chintcl  26997  spanval  26998  omlsi  27069  pjoml  27101  chnlen0  27109  chsscon3  27165  chlejb1  27177  chnle  27179  spanun  27210  h1datom  27247  cmbr4i  27266  pjoml2  27276  pjoml3  27277  lecm  27282  osumcor2i  27309  osum  27310  spansncv  27318  pjcjt2  27357  pjopyth  27385  hstel2  27884  stj  27900  stcltr1i  27939  mdi  27960  mdbr3  27962  mdbr4  27963  dmdbr  27964  dmdmd  27965  dmdbr5  27973  mdsl1i  27986  mdslmd1lem3  27992  mdslmd1lem4  27993  mdslmd1i  27994  csmdsymi  27999  atss  28011  atom1d  28018  superpos  28019  chcv1  28020  shatomici  28023  shatomistici  28026  hatomistici  28027  chrelat2  28035  chirredi  28059  atcvat4i  28062  mdsymlem2  28069  mdsymlem6  28073  dmdbr6ati  28088  dmdbr7ati  28089  gsumle  28549  gsumvsca1  28552  gsumvsca2  28553  xrge0tsmsd  28555  tpr2rico  28725  issiga  28940  isrnsigaOLD  28941  isrnsiga  28942  sigagenval  28969  measiuns  29046  dya2icoseg  29105  dya2iocnrect  29109  dya2iocuni  29111  carsgmon  29152  carsgsigalem  29153  carsgclctunlem2  29157  carsgclctun  29159  pmeasmono  29163  pmeasadd  29164  bnj517  29702  bnj1118  29799  bnj1145  29808  bnj1154  29814  bnj1452  29867  bnj1498  29876  kur14lem1  29935  cvmopnlem  30007  dfon2lem3  30437  dfon2lem7  30441  frmin  30486  frrlem1  30520  frrlem3  30522  brsset  30662  fness  31011  fneref  31012  fnessref  31019  neibastop2lem  31022  topmeet  31026  fnejoin2  31031  tailfb  31039  filnetlem4  31043  onsucsuccmpi  31109  bj-snglss  31566  dissneqlem  31744  relowlssretop  31768  relowlpssretop  31769  ptrecube  31942  poimirlem29  31971  mblfinlem2  31980  mblfinlem3  31981  mblfinlem4  31982  ismblfin  31983  ovoliunnfl  31984  voliunnfl  31986  volsupnfl  31987  indexa  32062  indexdom  32063  neificl  32084  istotbnd3  32105  sstotbnd2  32108  sstotbnd  32109  equivtotbnd  32112  ssbnd  32122  heiborlem1  32145  heiborlem6  32150  heiborlem8  32152  heiborlem10  32154  unichnidl  32266  pridl  32272  ismaxidl  32275  igenval  32296  igenval2  32301  ispridlc  32305  lsmsat  32576  lssatomic  32579  lssats  32580  lsat0cv  32601  lcvexchlem4  32605  lcvexchlem5  32606  lsatcvatlem  32617  l1cvpat  32622  ispsubsp  33312  linepsubN  33319  pclvalN  33457  ispsubclN  33504  ispsubcl2N  33514  pclfinclN  33517  diaelrnN  34615  docavalN  34693  dochval  34921  dvh4dimat  35008  dochexmidlem1  35030  lpolconN  35057  mapdordlem2  35207  ismrcd1  35542  ismrcd2  35543  ismrc  35545  mzpcompact2lem  35595  aomclem6  35919  hbtlem6  35990  rgspnval  36036  ssficl  36175  ssuncl  36176  ssdifcl  36177  sssymdifcl  36178  elmapintrab  36184  clcnvlem  36232  iunrelexpmin1  36302  iunrelexpmin2  36306  onfrALTlem5  36909  onfrALTlem5VD  37279  islptre  37741  dvmptconst  37827  dvmptidg  37829  dvmulcncf  37839  dvdivcncf  37841  dvmptfprod  37862  stoweidlem51  37969  stoweidlem52  37970  fourierdlem103  38130  fourierdlem104  38131  salgenval  38239  ovnval2  38430  ovncvrrp  38449  ovnsubaddlem1  38455  ovnsubadd  38457  ovncvr2  38496  hspmbl  38514  lpvtx  39257  umgredgprv  39295  usgredgprvALT  39378  issubgr2  39446  subgrprop2  39448  egrsubgr  39451  0uhgrsubgr  39453