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

Theorem sseq2 3213
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 3199 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 27 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3199 . . . 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 3207 . 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 1632    C_ wss 3165
This theorem is referenced by:  sseq12  3214  sseq2i  3216  sseq2d  3219  syl5sseq  3239  nssne1  3247  psseq2  3277  sseq0  3499  un00  3503  disjpss  3518  pweq  3641  ssintab  3895  ssintub  3896  intmin  3898  treq  4135  ssexg  4176  intabs  4188  ordunidif  4456  ordssun  4508  iunpw  4586  tfindsg  4667  limomss  4677  findsg  4699  fununi  5332  funcnvuni  5333  feq3  5393  ssimaexg  5601  frxp  6241  onfununi  6374  oawordeu  6569  oawordexr  6570  nnawordex  6651  ereq1  6683  xpider  6746  domeng  6892  sbthlem4  6990  sbthlem5  6991  domssex  7038  finsschain  7178  dffi2  7192  dffi3  7200  hartogslem1  7273  inf3lema  7341  cantnflem1  7407  tz9.1  7427  tz9.1c  7428  tctr  7441  tcmin  7442  tcrank  7570  scottex  7571  cardlim  7621  infxpenlem  7657  infxpenc2  7665  isinfcard  7735  alephinit  7738  alephval3  7753  dfac3  7764  cflem  7888  cfval  7889  cflecard  7895  cfsuc  7899  cff1  7900  cfflb  7901  cflim2  7905  isf32lem2  7996  fin1a2lem13  8054  ac7g  8117  ttukeylem5  8156  ttukeylem7  8158  pwcfsdom  8221  pwfseqlem5  8301  pwfseq  8302  gch2  8317  winalim  8333  wunex  8377  wuncss  8383  eltskg  8388  eltsk2g  8389  gruina  8456  grur1a  8457  axgroth6  8466  mrcflem  13524  mrcval  13528  isacs2  13571  acsfiel  13572  ipoval  14273  fpwipodrs  14283  ipodrsima  14284  mreclat  14306  slwispgp  14938  pgpssslw  14941  lsmss1b  14992  lsmss2b  14994  lspf  15747  lspval  15748  lbsextlem1  15927  lbsextlem3  15929  lbsextlem4  15930  aspval  16084  mplsubglem  16195  mpllsslem  16196  basis2  16705  eltg2  16712  clsval  16790  clscld  16800  clsval2  16803  ntrcls0  16829  isnei  16856  neiint  16857  neips  16866  opnneissb  16867  opnssneib  16868  neindisj2  16876  innei  16878  restcls  16927  cnpimaex  17002  cnprest2  17034  regsep  17078  nrmsep3  17099  nrmsep  17101  regsep2  17120  tgcmp  17144  uncmp  17146  1stcfb  17187  1stcrest  17195  2ndcctbss  17197  1stcelcls  17203  lly1stc  17238  xkoopn  17300  txcnp  17330  txcmplem1  17351  kqnrmlem1  17450  kqnrmlem2  17451  nrmhmph  17501  fbssfi  17548  opnfbas  17553  fbasfip  17579  fbunfip  17580  fgss2  17585  fgcl  17589  supfil  17606  isufil2  17619  filssufilg  17622  ssufl  17629  ufileu  17630  elfm3  17661  fmfnfm  17669  ufldom  17673  fbflim2  17688  flfneii  17703  flftg  17707  txflf  17717  supnfcls  17731  fclscf  17736  fclsfnflim  17738  flimfnfcls  17739  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  tsmsfbas  17826  tsmsres  17842  tsmsf1o  17843  tsmsxplem1  17851  tsmsxp  17853  blss  17988  metss  18070  metrest  18086  metcnp3  18102  metnrmlem3  18381  lebnumlem3  18477  lebnum  18478  ellimc3  19245  lhop1lem  19376  dchrelbas  20491  avril1  20852  resgrprn  20963  spanval  21928  spancl  21931  shsval2i  21982  omlsi  21999  ococin  22003  chsupsn  22008  pjoml  22031  shs00i  22045  chj00i  22082  chsscon3  22095  chlejb1  22107  chnle  22109  pjoml2  22206  pjoml3  22207  lecm  22212  stcltr1i  22870  mdbr  22890  dmdmd  22896  dmdi  22898  dmdbr3  22901  dmdbr4  22902  mdsl1i  22917  mdslmd1lem3  22923  mdslmd1lem4  22924  csmdsymi  22930  hatomic  22956  chrelat2  22966  atord  22984  atcvat4i  22993  iundifdifd  23175  iundifdif  23176  sigagenval  23516  dmsigagen  23520  sigagenss  23525  kur14lem9  23760  dfrtrcl2  24060  wfrlem1  24327  wfrlem4  24330  wfrlem15  24341  frrlem1  24352  frrlem4  24355  frrlem5e  24360  frrlem11  24364  altopthsn  24567  bpolyval  24856  prjpacp1  25230  prjpacp2  25231  relinccppr  25232  sssu  25244  prl  25270  prjmapcp2  25273  inposetlem  25379  inposet  25381  dominc  25383  domncnt  25385  svs2  25590  unint2t  25621  intfmu2  25622  osneisi  25634  intopcoaconlem3b  25641  intopcoaconlem3  25642  efilcp  25655  fgsb2  25658  limptlimpr2lem1  25677  limptlimpr2lem2  25678  islimrs  25683  bwt2  25695  hdrmp  25809  algi  25830  partarelt1  25999  partarelt2  26000  indcls2  26099  pfsubkl  26150  bisig0  26165  iscol3  26197  ssref  26386  refref  26388  fnessref  26396  refssfne  26397  comppfsc  26410  topjoin  26417  neifg  26423  totbndss  26604  heibor1lem  26636  unichnidl  26759  ispridl  26762  maxidlmax  26771  igenval  26789  igenidl  26791  igenmin  26792  igenval2  26794  nacsfix  26890  mzpcompact2  26933  rgspnval  27476  rgspncl  27477  rgspnmin  27479  ssrecnpr  27640  bnj1286  29365  bnj1452  29398  lsatcmp  29815  lcvexchlem4  29849  lcvexchlem5  29850  pclvalN  30701  pclclN  30702  elpcliN  30704  docaclN  31936  dihglb2  32154  doch2val2  32176  dochocss  32178  dochexmidlem7  32278  lpolconN  32299  mapdval  32440
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator