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

Theorem sseq2 3330
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 3315 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 29 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3315 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 29 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 550 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3323 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 610 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 258 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    C_ wss 3280
This theorem is referenced by:  sseq12  3331  sseq2i  3333  sseq2d  3336  syl5sseq  3356  nssne1  3364  psseq2  3395  sseq0  3619  un00  3623  disjpss  3638  pweq  3762  ssintab  4027  ssintub  4028  intmin  4030  treq  4268  ssexg  4309  intabs  4321  ordunidif  4589  ordssun  4640  iunpw  4718  tfindsg  4799  limomss  4809  findsg  4831  fununi  5476  funcnvuni  5477  feq3  5537  ssimaexg  5748  frxp  6415  onfununi  6562  oawordeu  6757  oawordexr  6758  nnawordex  6839  ereq1  6871  xpider  6934  domeng  7081  sbthlem4  7179  sbthlem5  7180  domssex  7227  finsschain  7371  dffi2  7386  dffi3  7394  hartogslem1  7467  inf3lema  7535  cantnflem1  7601  tz9.1  7621  tz9.1c  7622  tctr  7635  tcmin  7636  tcrank  7764  scottex  7765  cardlim  7815  infxpenlem  7851  infxpenc2  7859  isinfcard  7929  alephinit  7932  alephval3  7947  dfac3  7958  cflem  8082  cfval  8083  cflecard  8089  cfsuc  8093  cff1  8094  cfflb  8095  cflim2  8099  isf32lem2  8190  fin1a2lem13  8248  ac7g  8310  ttukeylem5  8349  ttukeylem7  8351  pwcfsdom  8414  pwfseqlem5  8494  pwfseq  8495  gch2  8510  winalim  8526  wunex  8570  wuncss  8576  eltskg  8581  eltsk2g  8582  gruina  8649  grur1a  8650  axgroth6  8659  mrcflem  13786  mrcval  13790  isacs2  13833  acsfiel  13834  ipoval  14535  fpwipodrs  14545  ipodrsima  14546  mreclat  14568  slwispgp  15200  pgpssslw  15203  lsmss1b  15254  lsmss2b  15256  lspf  16005  lspval  16006  lbsextlem1  16185  lbsextlem3  16187  lbsextlem4  16188  aspval  16342  mplsubglem  16453  mpllsslem  16454  basis2  16971  eltg2  16978  clsval  17056  clscld  17066  clsval2  17069  ntrcls0  17095  isnei  17122  neiint  17123  neips  17132  opnneissb  17133  opnssneib  17134  neindisj2  17142  innei  17144  neiptoptop  17150  neiptopnei  17151  neitr  17198  restcls  17199  cnpimaex  17274  cnprest2  17308  regsep  17352  nrmsep3  17373  nrmsep  17375  regsep2  17394  tgcmp  17418  uncmp  17420  1stcfb  17461  1stcrest  17469  2ndcctbss  17471  1stcelcls  17477  lly1stc  17512  xkoopn  17574  neitx  17592  txcnp  17605  txcmplem1  17626  kqnrmlem1  17728  kqnrmlem2  17729  nrmhmph  17779  fbssfi  17822  opnfbas  17827  fbasfip  17853  fbunfip  17854  fgss2  17859  fgcl  17863  supfil  17880  isufil2  17893  filssufilg  17896  ssufl  17903  ufileu  17904  elfm3  17935  fmfnfm  17943  ufldom  17947  fbflim2  17962  flfneii  17977  flftg  17981  txflf  17991  supnfcls  18005  fclscf  18010  fclsfnflim  18012  flimfnfcls  18013  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  tsmsfbas  18110  tsmsres  18126  tsmsf1o  18127  tsmsxplem1  18135  tsmsxp  18137  ustssel  18188  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  ust0  18202  elutop  18216  ustuqtop4  18227  cfiluexsm  18273  cfiluweak  18278  blssps  18407  blss  18408  metss  18491  metrest  18507  metcnp3  18523  metnrmlem3  18844  lebnumlem3  18941  lebnum  18942  ellimc3  19719  lhop1lem  19850  dchrelbas  20973  avril1  21710  resgrprn  21821  spanval  22788  spancl  22791  shsval2i  22842  omlsi  22859  ococin  22863  chsupsn  22868  pjoml  22891  shs00i  22905  chj00i  22942  chsscon3  22955  chlejb1  22967  chnle  22969  pjoml2  23066  pjoml3  23067  lecm  23072  stcltr1i  23730  mdbr  23750  dmdmd  23756  dmdi  23758  dmdbr3  23761  dmdbr4  23762  mdsl1i  23777  mdslmd1lem3  23783  mdslmd1lem4  23784  csmdsymi  23790  hatomic  23816  chrelat2  23826  atord  23844  atcvat4i  23853  sigagenval  24476  dmsigagen  24480  sigagenss  24485  kur14lem9  24853  dfrtrcl2  25101  fprodss  25227  wfrlem1  25470  wfrlem4  25473  wfrlem15  25484  frrlem1  25495  frrlem4  25498  frrlem5e  25503  frrlem11  25507  altopthsn  25710  bpolyval  25999  mblfinlem2  26144  ssref  26253  refref  26255  fnessref  26263  refssfne  26264  comppfsc  26277  topjoin  26284  neifg  26290  totbndss  26376  heibor1lem  26408  unichnidl  26531  ispridl  26534  maxidlmax  26543  igenval  26561  igenidl  26563  igenmin  26564  igenval2  26566  nacsfix  26656  mzpcompact2  26699  rgspnval  27241  rgspncl  27242  rgspnmin  27244  ssrecnpr  27405  bnj1286  29094  bnj1452  29127  lsatcmp  29486  lcvexchlem4  29520  lcvexchlem5  29521  pclvalN  30372  pclclN  30373  elpcliN  30375  docaclN  31607  dihglb2  31825  doch2val2  31847  dochocss  31849  dochexmidlem7  31949  lpolconN  31970  mapdval  32111
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator