MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseq2 Structured version   Unicode version

Theorem sseq2 3508
Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
Assertion
Ref Expression
sseq2  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )

Proof of Theorem sseq2
StepHypRef Expression
1 sstr2 3493 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 31 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3493 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 31 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 566 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3501 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 628 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 266 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
Colors of variables: wff setvar class
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  sseq2i  3511  sseq2d  3514  syl5sseq  3534  nssne1  3542  psseq2  3574  sseq0  3799  un00  3844  disjpss  3859  pweq  3996  ssintab  4284  ssintub  4285  intmin  4287  treq  4532  sseliALT  4564  ssexg  4579  intabs  4594  ordunidif  4912  ordssun  4963  fununi  5640  feq3  5701  ssimaexg  5920  iunpw  6595  tfindsg  6676  limomss  6686  findsg  6708  funcnvuni  6734  frxp  6891  onfununi  7010  oawordeu  7202  oawordexr  7203  nnawordex  7284  ereq1  7316  xpider  7380  domeng  7528  sbthlem4  7628  sbthlem5  7629  domssex  7676  finsschain  7825  dffi2  7881  dffi3  7889  hartogslem1  7965  inf3lema  8039  cantnflem1  8106  cantnflem1OLD  8129  tz9.1  8158  tz9.1c  8159  tctr  8169  tcmin  8170  tcrank  8300  scottex  8301  cardlim  8351  infxpenlem  8389  infxpenc2  8397  infxpenc2OLD  8401  isinfcard  8471  alephinit  8474  alephval3  8489  dfac3  8500  cflem  8624  cfval  8625  cflecard  8631  cfsuc  8635  cff1  8636  cfflb  8637  cflim2  8641  isf32lem2  8732  fin1a2lem13  8790  ac7g  8852  ttukeylem5  8891  ttukeylem7  8893  pwcfsdom  8956  pwfseqlem5  9039  pwfseq  9040  gch2  9051  winalim  9071  wunex  9115  wuncss  9121  eltskg  9126  eltsk2g  9127  gruina  9194  grur1a  9195  axgroth6  9204  swrdvalodm2  12638  swrdvalodm  12639  mrcflem  14875  mrcval  14879  isacs2  14922  acsfiel  14923  ipoval  15653  fpwipodrs  15663  ipodrsima  15664  mreclatBAD  15686  slwispgp  16500  pgpssslw  16503  lsmss1b  16554  lsmss2b  16556  cntzcmnss  16718  gsumzres  16783  lspf  17488  lspval  17489  lbsextlem1  17672  lbsextlem3  17674  lbsextlem4  17675  aspval  17845  mplsubglem  17961  mpllsslem  17962  mplsubglemOLD  17963  mpllsslemOLD  17964  basis2  19319  eltg2  19326  clsval  19404  clscld  19414  clsval2  19417  ntrcls0  19443  isnei  19470  neiint  19471  neips  19480  opnneissb  19481  opnssneib  19482  neindisj2  19490  innei  19492  neiptoptop  19498  neiptopnei  19499  neitr  19547  restcls  19548  cnpimaex  19623  cnprest2  19657  regsep  19701  nrmsep3  19722  nrmsep  19724  regsep2  19743  tgcmp  19767  uncmp  19769  bwth  19776  bwthOLD  19777  1stcfb  19812  1stcrest  19820  2ndcctbss  19822  1stcelcls  19828  lly1stc  19863  ssref  19879  refref  19880  comppfsc  19899  xkoopn  19956  neitx  19974  txcnp  19987  txcmplem1  20008  kqnrmlem1  20110  kqnrmlem2  20111  nrmhmph  20161  fbssfi  20204  opnfbas  20209  fbasfip  20235  fbunfip  20236  fgss2  20241  fgcl  20245  supfil  20262  isufil2  20275  filssufilg  20278  ssufl  20285  ufileu  20286  elfm3  20317  fmfnfm  20325  ufldom  20329  fbflim2  20344  flfneii  20359  flftg  20363  txflf  20373  supnfcls  20387  fclscf  20392  fclsfnflim  20394  flimfnfcls  20395  alexsubALTlem2  20414  alexsubALTlem3  20415  alexsubALTlem4  20416  alexsubALT  20417  tsmsfbas  20492  tsmsresOLD  20511  tsmsres  20512  tsmsf1o  20513  tsmsxplem1  20521  tsmsxp  20523  ustssel  20574  ustincl  20576  ustdiag  20577  ustinvel  20578  ustexhalf  20579  ust0  20588  elutop  20602  ustuqtop4  20613  cfiluexsm  20659  cfiluweak  20664  blssps  20793  blss  20794  metss  20877  metrest  20893  metcnp3  20909  metnrmlem3  21231  lebnumlem3  21329  lebnum  21330  ellimc3  22149  lhop1lem  22280  dchrelbas  23376  avril1  25036  resgrprn  25147  spanval  26116  spancl  26119  shsval2i  26170  omlsi  26187  ococin  26191  chsupsn  26196  pjoml  26219  shs00i  26233  chj00i  26270  chsscon3  26283  chlejb1  26295  chnle  26297  pjoml2  26394  pjoml3  26395  lecm  26400  stcltr1i  27058  mdbr  27078  dmdmd  27084  dmdi  27086  dmdbr3  27089  dmdbr4  27090  mdsl1i  27105  mdslmd1lem3  27111  mdslmd1lem4  27112  csmdsymi  27118  hatomic  27144  chrelat2  27154  atord  27172  atcvat4i  27181  reff  27708  cmpcref  27719  sigagenval  28006  dmsigagen  28010  sigagenss  28015  kur14lem9  28524  mclsssvlem  28788  mclsind  28796  dfrtrcl2  28937  fprodss  29048  wrecseq123  29305  wfrlem1  29311  wfrlem4  29314  wfrlem15  29325  frrlem1  29355  frrlem4  29358  frrlem5e  29363  frrlem11  29367  imagesset  29571  altopthsn  29579  mblfinlem3  30021  fnessref  30143  refssfne  30144  topjoin  30151  neifg  30157  totbndss  30241  heibor1lem  30273  unichnidl  30396  ispridl  30399  maxidlmax  30408  igenval  30426  igenidl  30428  igenmin  30429  igenval2  30431  nacsfix  30612  mzpcompact2  30653  rgspnval  31086  rgspncl  31087  rgspnmin  31089  ssrecnpr  31157  islptre  31529  bnj1286  33782  bnj1452  33815  bj-snglex  34243  lsatcmp  34430  lcvexchlem4  34464  lcvexchlem5  34465  pclvalN  35316  pclclN  35317  elpcliN  35319  docaclN  36553  dihglb2  36771  doch2val2  36793  dochocss  36795  dochexmidlem7  36895  lpolconN  36916  mapdval  37057  superficl  37417  superuncl  37418  trclub  37439  trclubg  37440
  Copyright terms: Public domain W3C validator