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

Theorem sseq2 3422
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 3407 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 32 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3407 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 32 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 568 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3415 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 632 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 269 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3379  df-ss 3386
This theorem is referenced by:  sseq12  3423  sseq2i  3425  sseq2d  3428  syl5sseq  3448  nssne1  3456  psseq2  3489  sseq0  3732  un00  3766  disjpss  3781  pweq  3920  ssintab  4208  ssintub  4209  intmin  4211  treq  4460  sseliALT  4493  ssexg  4506  intabs  4521  ordunidif  5426  ordssun  5477  fununi  5603  feq3  5666  ssimaexg  5884  iunpw  6556  tfindsg  6638  limomss  6648  findsg  6671  funcnvuni  6697  frxp  6854  wrecseq123  6977  wfrlem1  6983  wfrlem4  6987  wfrlem15  6998  onfununi  7008  oawordeu  7204  oawordexr  7205  nnawordex  7286  ereq1  7318  xpider  7382  domeng  7531  sbthlem4  7631  sbthlem5  7632  domssex  7679  finsschain  7827  dffi2  7883  dffi3  7891  hartogslem1  8003  inf3lema  8075  cantnflem1  8139  tz9.1  8158  tz9.1c  8159  tctr  8169  tcmin  8170  tcrank  8300  scottex  8301  cardlim  8351  infxpenlem  8389  infxpenc2  8397  isinfcard  8467  alephinit  8470  alephval3  8485  dfac3  8496  cflem  8620  cfval  8621  cflecard  8627  cfsuc  8631  cff1  8632  cfflb  8633  cflim2  8637  isf32lem2  8728  fin1a2lem13  8786  ac7g  8848  ttukeylem5  8887  ttukeylem7  8889  pwcfsdom  8952  pwfseqlem5  9032  pwfseq  9033  gch2  9044  winalim  9064  wunex  9108  wuncss  9114  eltskg  9119  eltsk2g  9120  gruina  9187  grur1a  9188  axgroth6  9197  swrdnd2  12728  trcleq2lem  12992  dfrtrcl2  13062  fprodss  13938  mrcflem  15448  mrcval  15452  isacs2  15495  acsfiel  15496  ipoval  16336  fpwipodrs  16346  ipodrsima  16347  mreclatBAD  16369  slwispgp  17199  pgpssslw  17202  lsmss1b  17253  lsmss2b  17255  cntzcmnss  17417  gsumzres  17479  lspf  18133  lspval  18134  lbsextlem1  18317  lbsextlem3  18319  lbsextlem4  18320  aspval  18488  mplsubglem  18594  mpllsslem  18595  basis2  19901  eltg2  19908  clsval  19987  clscld  19997  clsval2  20000  ntrcls0  20027  isnei  20054  neiint  20055  neips  20064  opnneissb  20065  opnssneib  20066  neindisj2  20074  innei  20076  neiptoptop  20082  neiptopnei  20083  neitr  20131  restcls  20132  cnpimaex  20207  cnprest2  20241  regsep  20285  nrmsep3  20306  nrmsep  20308  regsep2  20327  tgcmp  20351  uncmp  20353  bwth  20360  1stcfb  20395  1stcrest  20403  2ndcctbss  20405  1stcelcls  20411  lly1stc  20446  ssref  20462  refref  20463  comppfsc  20482  xkoopn  20539  neitx  20557  txcnp  20570  txcmplem1  20591  kqnrmlem1  20693  kqnrmlem2  20694  nrmhmph  20744  fbssfi  20787  opnfbas  20792  fbasfip  20818  fbunfip  20819  fgss2  20824  fgcl  20828  supfil  20845  isufil2  20858  filssufilg  20861  ssufl  20868  ufileu  20869  elfm3  20900  fmfnfm  20908  ufldom  20912  fbflim2  20927  flfneii  20942  flftg  20946  txflf  20956  supnfcls  20970  fclscf  20975  fclsfnflim  20977  flimfnfcls  20978  alexsubALTlem2  20998  alexsubALTlem3  20999  alexsubALTlem4  21000  alexsubALT  21001  tsmsfbas  21077  tsmsres  21093  tsmsf1o  21094  tsmsxplem1  21102  tsmsxp  21104  ustssel  21155  ustincl  21157  ustdiag  21158  ustinvel  21159  ustexhalf  21160  ust0  21169  elutop  21183  ustuqtop4  21194  cfiluexsm  21240  cfiluweak  21245  blssps  21374  blss  21375  metss  21458  metrest  21474  metcnp3  21490  metnrmlem3  21813  metnrmlem3OLD  21828  lebnumlem3  21926  lebnumlem3OLD  21929  lebnum  21930  ellimc3  22769  lhop1lem  22900  dchrelbas  24099  avril1  25835  resgrprn  25943  spanval  26921  spancl  26924  shsval2i  26975  omlsi  26992  ococin  26996  chsupsn  27001  pjoml  27024  shs00i  27038  chj00i  27075  chsscon3  27088  chlejb1  27100  chnle  27102  pjoml2  27199  pjoml3  27200  lecm  27205  stcltr1i  27862  mdbr  27882  dmdmd  27888  dmdi  27890  dmdbr3  27893  dmdbr4  27894  mdsl1i  27909  mdslmd1lem3  27915  mdslmd1lem4  27916  csmdsymi  27922  hatomic  27948  chrelat2  27958  atord  27976  atcvat4i  27985  fz1nntr  28321  reff  28611  cmpcref  28622  sigagenval  28907  dmsigagen  28911  sigagenss  28916  ldsysgenld  28927  ldgenpisyslem1  28930  ldgenpisyslem2  28931  dynkin  28934  carsgmon  29091  carsgclctunlem2  29096  bnj1286  29773  bnj1452  29806  kur14lem9  29882  mclsssvlem  30145  mclsind  30153  frrlem1  30458  frrlem4  30461  frrlem5e  30466  frrlem11  30470  imagesset  30662  altopthsn  30670  fnessref  30955  refssfne  30956  topjoin  30963  neifg  30969  bj-snglex  31472  relowlssretop  31667  relowlpssretop  31668  finxpreclem3  31686  poimirlem29  31870  poimir  31874  mblfinlem3  31880  totbndss  32010  heibor1lem  32042  unichnidl  32165  ispridl  32168  maxidlmax  32177  igenval  32195  igenidl  32197  igenmin  32198  igenval2  32200  lsatcmp  32475  lcvexchlem4  32509  lcvexchlem5  32510  pclvalN  33361  pclclN  33362  elpcliN  33364  docaclN  34598  dihglb2  34816  doch2val2  34838  dochocss  34840  dochexmidlem7  34940  lpolconN  34961  mapdval  35102  nacsfix  35460  mzpcompact2  35500  rgspnval  35941  rgspncl  35942  rgspnmin  35944  superficl  36078  superuncl  36079  cleq2lem  36121  clcnvlem  36137  dfrtrcl3  36232  ssrecnpr  36563  founiiun  37344  founiiun0  37363  islptre  37576  iunopeqop  38807  dfnbgr3  39138  nbupgr  39142  nbumgrvtx  39144  nbgr2vtx1edg  39148  nbuhgr2vtx1edgb  39150  cusgrexi  39229
  Copyright terms: Public domain W3C validator