Theorem sseq1 2637

Description: Equality theorem for subclasses. (The proof was 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 2631	. 2 |- (A = B <-> (A C_ B /\ B C_ A))
2		sstr2 2623	. . . 4 |- (B C_ A -> (A C_ C -> B C_ C))
3	2	adantl 424	. . 3 |- ((A C_ B /\ B C_ A) -> (A C_ C -> B C_ C))
4		sstr2 2623	. . . 4 |- (A C_ B -> (B C_ C -> A C_ C))
5	4	adantr 425	. . 3 |- ((A C_ B /\ B C_ A) -> (B C_ C -> A C_ C))
6	3, 5	impbid 574	. 2 |- ((A C_ B /\ B C_ A) -> (A C_ C <-> B C_ C))
7	1, 6	sylbi 216	1 |- (A = B -> (A C_ C <-> B C_ C))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   C_ wss 2593

This theorem is referenced by:  sseq12 2640  sseq1i 2641  sseq1d 2644  psseq1 2697  sbss 2980  pwjust 3033  elpw 3037  elpwg 3038  pwpw0 3134  sssn 3142  sspr 3144  prsspwOLD 3151  pwsnALT 3173  unimax 3212  trss 3421  elssabg 3462  intabs 3469  nnullss 3515  exss 3516  fri 3626  frc 3629  rabsnt 3821  onssmin 3878  releq 4071  iss 4254  issOLD 4255  fununi 4481  funcnvuni 4482  fssxpOLD 4576  ffoss 4665  ssimaex 4729  isofrlem 4878  f1oweALT 4883  tfrlem1 5119  oawordeu 5237  elpm 5395  pw2en 5505  sbthlem2 5511  sbth 5520  php 5607  unbnn2 5638  fiint 5650  abfii3 5653  abfii4 5654  hartog 5693  sucprcreg 5703  unbnn3 5746  tz9.1 5753  setind 5759  rankr1 5785  rankr1id 5808  scott0 5847  bnd2 5854  omsubinit 5890  aceq3lem 5894  ac6lem 5916  zorn2lem7 5956  oncard 5978  carduni 6010  cardaleph 6033  cflem 6053  cflim 6057  cflecard 6060  cfeq0 6062  cfsuc 6063  infxpidmlem2 8822  infxpidmlem3 8823  infxpidmlem7 8827  infxpidmlem8 8828  infmap2lem1 8848  infmap2 8850  uniopn 8867  fiinbas 8885  eltg2 8889  tgval3 8895  topbas 8897  subbas 8914  subbas2 8915  subtop 8916  fctop 8920  cctop 8922  retopbas 8925  txuni 8935  iscld 8945  clsval 8953  clsval2 8961  neival 8993  isnei 8994  neiint 8995  neips 9003  opnneissb 9004  opnssneib 9005  innei 9012  islp2 9023  dnsconst 9065  blssex 9131  opnm 9137  blssopn 9144  opnin 9146  neibl 9154  lmbr 9206  bcthlem7 9283  issubg 9425  vacnlem4 9670  grothomex 10136  axgroth6 10137  axgroth3 10138  axgroth4 10139  twpar2 10149  indexfi 10174  fiv 10212  fine 10213  fiuni 10219  fiiu2 10220  elsubsp 10248  stoig 10251  subcld 10254  subtopmetlem 10255  fillsb 10270  fipfil2 10272  oefil2 10275  filfbas 10276  fbssint 10279  infi 10280  fsubbas 10281  fbunfip 10282  fbssfg 10285  fbfgss 10288  fgfil 10290  extbas1 10291  filrn 10293  filmapss 10309  elfilmap 10312  sh 10711  hhsssh 10772  occl 10815  omlsi 10879  pjoml 10902  shintcl 10927  chintcl 10929  spanval 10932  shlub 10987  chnlen0 11001  chsscon3 11056  chlejb1 11068  chnle 11070  spanun 11101  h1datom 11138  cmbr4i 11177  pjoml2 11187  pjoml3 11188  lecm 11193  osumlem8 11220  osum 11223  osumcor2i 11225  spansncv 11233  pjcjt2 11272  pjopyth 11300  pjss1coi 11735  hstel2 11791  stj 11807  stcltr1i 11846  mdi 11867  mdbr3 11869  mdbr4 11870  dmdbr 11871  dmdmd 11872  dmdbr5 11880  mdsl1i 11893  mdslmd1lem3 11899  mdslmd1lem4 11900  mdslmd1i 11901  csmdsymi 11906  atss 11918  atom1d 11925  superpos 11926  chcv1 11927  shatomici 11930  shatomistici 11933  hatomistici 11934  chrelat2 11942  atcvatlem 11957  irredi 11966  atcvat4i 11969  mdsymlem2 11976  mdsymlem3 11977  mdsymlem6 11980  dmdbr6ati 11995  dmdbr7ati 11996  bnj1117 12927  bnj1143 12942  bnj218 13250  bnj1145 13431  bnj1154 13438  bnj1462 13546  dfon2lem3 13851  dfon2lem7 13855  dford4lem1 13859  tz6.26 13913  trclss 13935  frmin 13938  frxp 13951  wfrlem1 13957  wfrlem4 13960  wfrlem15 13971  axfelem16 14046  brsset 14069  infi1 14343  fiiu 14344  ficli 14353  scprefat 14380  scprefat2 14381  twsymr 14394  imfstnrelc 14396  reflincror 14446  reltrncnv 14457  int2pre 14578  posprs 14581  inposetlem 14618  inposet 14620  rninc 14623  ranncnt 14625  dfps2 14634  svs2 14829  svs3 14830  oibbi1 14853  oibbi2 14854  sallnei 14873  osneisi 14875  qusp 14908  fgsb 14921  efilcp 14922  filint2 14923  fgsb2 14925  efilcp2 14926  cnfilca 14927  rcfpfillem3 14930  rcfpfillem4 14931  rcfpfillem5 14932  rcfpfillem6 14933  rcfpfil 14934  clindistop 14962  altretoplem2 14996  altretop 14997  dualalg 15131  infemb 15207  tmpts 15257  vtarsuelt 15272  elfiun 15369  fictb 15371  inficlALT 15372  finsschain 15373  hartogOLD 15384  omsubinitOLD 15399  ssntr 15405  cncls 15419  cnntr 15420  subcls 15424  subntr 15425  compsublem 15430  compsub 15431  hscptsscld 15434  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  alexsub 15441  connsub 15443  2ndcsb 15476  2ndc1stc 15477  2ndcctbss 15478  isfne3 15482  refssex 15490  fness 15491  fneref 15493  fnessref 15503  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  topmeet 15526  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  regsep 15550  nrmsep 15554  nrmsep2 15555  opnfbas 15557  supfil 15560  filfinnfr 15561  filssufillem 15570  filssufil 15571  uffixfr 15575  ufinffr 15578  ufilen 15579  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfm 15598  fcluscf 15612  flimfnfcls 15615  fcluscnplem 15617  fcluscomplem 15620  tailfb 15639  filnetlem1 15640  filnetlem2 15641  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  fimax 15746  indexa 15753  indexdom 15754  indexfiOLD 15755  inficl 15757  zornn0 15764  neificl 15841  sstotbnd 15936  totbndss 15937  ismtyhmeolem 15950  heiborlem1 15955  heiborlem20 15974  heiborlem21 15975  heiborlem23 15977  heiborlem42 15996  rrntotbnd 16022  unichnidl 16179  pridl 16185  ismaxidl 16188  igenval 16209  igenval2 16214  ispridlc 16218  ishgrag 16291  hgralem 16292  ispgrag 16301  clatlem 16889  clatlat 16893  iscsubsp 17209  ispsubsp 17226  linepsub 17232  ispsubcl 17347  ispsubcl2 17356

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain