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

Theorem sseq2 3200
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 3186 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 27 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3186 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 27 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 549 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3194 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 609 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 257 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    C_ wss 3152
This theorem is referenced by:  sseq12  3201  sseq2i  3203  sseq2d  3206  syl5sseq  3226  nssne1  3234  psseq2  3264  sseq0  3486  un00  3490  disjpss  3505  pweq  3628  ssintab  3879  ssintub  3880  intmin  3882  treq  4119  ssexg  4160  intabs  4172  ordunidif  4440  ordssun  4492  iunpw  4570  tfindsg  4651  limomss  4661  findsg  4683  fununi  5316  funcnvuni  5317  feq3  5377  ssimaexg  5585  frxp  6225  onfununi  6358  oawordeu  6553  oawordexr  6554  nnawordex  6635  ereq1  6667  xpider  6730  domeng  6876  sbthlem4  6974  sbthlem5  6975  domssex  7022  finsschain  7162  dffi2  7176  dffi3  7184  hartogslem1  7257  inf3lema  7325  cantnflem1  7391  tz9.1  7411  tz9.1c  7412  tctr  7425  tcmin  7426  tcrank  7554  scottex  7555  cardlim  7605  infxpenlem  7641  infxpenc2  7649  isinfcard  7719  alephinit  7722  alephval3  7737  dfac3  7748  cflem  7872  cfval  7873  cflecard  7879  cfsuc  7883  cff1  7884  cfflb  7885  cflim2  7889  isf32lem2  7980  fin1a2lem13  8038  ac7g  8101  ttukeylem5  8140  ttukeylem7  8142  pwcfsdom  8205  pwfseqlem5  8285  pwfseq  8286  gch2  8301  winalim  8317  wunex  8361  wuncss  8367  eltskg  8372  eltsk2g  8373  gruina  8440  grur1a  8441  axgroth6  8450  mrcflem  13508  mrcval  13512  isacs2  13555  acsfiel  13556  ipoval  14257  fpwipodrs  14267  ipodrsima  14268  mreclat  14290  slwispgp  14922  pgpssslw  14925  lsmss1b  14976  lsmss2b  14978  lspf  15731  lspval  15732  lbsextlem1  15911  lbsextlem3  15913  lbsextlem4  15914  aspval  16068  mplsubglem  16179  mpllsslem  16180  basis2  16689  eltg2  16696  clsval  16774  clscld  16784  clsval2  16787  ntrcls0  16813  isnei  16840  neiint  16841  neips  16850  opnneissb  16851  opnssneib  16852  neindisj2  16860  innei  16862  restcls  16911  cnpimaex  16986  cnprest2  17018  regsep  17062  nrmsep3  17083  nrmsep  17085  regsep2  17104  tgcmp  17128  uncmp  17130  1stcfb  17171  1stcrest  17179  2ndcctbss  17181  1stcelcls  17187  lly1stc  17222  xkoopn  17284  txcnp  17314  txcmplem1  17335  kqnrmlem1  17434  kqnrmlem2  17435  nrmhmph  17485  fbssfi  17532  opnfbas  17537  fbasfip  17563  fbunfip  17564  fgss2  17569  fgcl  17573  supfil  17590  isufil2  17603  filssufilg  17606  ssufl  17613  ufileu  17614  elfm3  17645  fmfnfm  17653  ufldom  17657  fbflim2  17672  flfneii  17687  flftg  17691  txflf  17701  supnfcls  17715  fclscf  17720  fclsfnflim  17722  flimfnfcls  17723  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  tsmsfbas  17810  tsmsres  17826  tsmsf1o  17827  tsmsxplem1  17835  tsmsxp  17837  blss  17972  metss  18054  metrest  18070  metcnp3  18086  metnrmlem3  18365  lebnumlem3  18461  lebnum  18462  ellimc3  19229  lhop1lem  19360  dchrelbas  20475  avril1  20836  resgrprn  20947  spanval  21912  spancl  21915  shsval2i  21966  omlsi  21983  ococin  21987  chsupsn  21992  pjoml  22015  shs00i  22029  chj00i  22066  chsscon3  22079  chlejb1  22091  chnle  22093  pjoml2  22190  pjoml3  22191  lecm  22196  stcltr1i  22854  mdbr  22874  dmdmd  22880  dmdi  22882  dmdbr3  22885  dmdbr4  22886  mdsl1i  22901  mdslmd1lem3  22907  mdslmd1lem4  22908  csmdsymi  22914  hatomic  22940  chrelat2  22950  atord  22968  atcvat4i  22977  iundifdifd  23159  iundifdif  23160  sigagenval  23501  dmsigagen  23505  sigagenss  23510  kur14lem9  23745  dfrtrcl2  24045  wfrlem1  24256  wfrlem4  24259  wfrlem15  24270  frrlem1  24281  frrlem4  24284  frrlem5e  24289  frrlem11  24293  altopthsn  24495  bpolyval  24784  prjpacp1  25127  prjpacp2  25128  relinccppr  25129  sssu  25141  prl  25167  prjmapcp2  25170  inposetlem  25276  inposet  25278  dominc  25280  domncnt  25282  svs2  25487  unint2t  25518  intfmu2  25519  osneisi  25531  intopcoaconlem3b  25538  intopcoaconlem3  25539  efilcp  25552  fgsb2  25555  limptlimpr2lem1  25574  limptlimpr2lem2  25575  islimrs  25580  bwt2  25592  hdrmp  25706  algi  25727  partarelt1  25896  partarelt2  25897  indcls2  25996  pfsubkl  26047  bisig0  26062  iscol3  26094  ssref  26283  refref  26285  fnessref  26293  refssfne  26294  comppfsc  26307  topjoin  26314  neifg  26320  totbndss  26501  heibor1lem  26533  unichnidl  26656  ispridl  26659  maxidlmax  26668  igenval  26686  igenidl  26688  igenmin  26689  igenval2  26691  nacsfix  26787  mzpcompact2  26830  rgspnval  27373  rgspncl  27374  rgspnmin  27376  ssrecnpr  27537  bnj1286  29049  bnj1452  29082  lsatcmp  29193  lcvexchlem4  29227  lcvexchlem5  29228  pclvalN  30079  pclclN  30080  elpcliN  30082  docaclN  31314  dihglb2  31532  doch2val2  31554  dochocss  31556  dochexmidlem7  31656  lpolconN  31677  mapdval  31818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator