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

Theorem sseq2 3511
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 3496 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 31 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3496 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 31 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 564 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3504 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 626 . 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 367    = wceq 1398    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  sseq12  3512  sseq2i  3514  sseq2d  3517  syl5sseq  3537  nssne1  3545  psseq2  3578  sseq0  3816  un00  3850  disjpss  3865  pweq  4002  ssintab  4288  ssintub  4289  intmin  4291  treq  4538  sseliALT  4570  ssexg  4583  intabs  4598  ordunidif  4915  ordssun  4966  fununi  5636  feq3  5697  ssimaexg  5914  iunpw  6587  tfindsg  6668  limomss  6678  findsg  6700  funcnvuni  6726  frxp  6883  onfununi  7004  oawordeu  7196  oawordexr  7197  nnawordex  7278  ereq1  7310  xpider  7374  domeng  7523  sbthlem4  7623  sbthlem5  7624  domssex  7671  finsschain  7819  dffi2  7875  dffi3  7883  hartogslem1  7959  inf3lema  8032  cantnflem1  8099  cantnflem1OLD  8122  tz9.1  8151  tz9.1c  8152  tctr  8162  tcmin  8163  tcrank  8293  scottex  8294  cardlim  8344  infxpenlem  8382  infxpenc2  8390  infxpenc2OLD  8394  isinfcard  8464  alephinit  8467  alephval3  8482  dfac3  8493  cflem  8617  cfval  8618  cflecard  8624  cfsuc  8628  cff1  8629  cfflb  8630  cflim2  8634  isf32lem2  8725  fin1a2lem13  8783  ac7g  8845  ttukeylem5  8884  ttukeylem7  8886  pwcfsdom  8949  pwfseqlem5  9030  pwfseq  9031  gch2  9042  winalim  9062  wunex  9106  wuncss  9112  eltskg  9117  eltsk2g  9118  gruina  9185  grur1a  9186  axgroth6  9195  swrdnd2  12652  trcleq2lem  12912  dfrtrcl2  12980  fprodss  13840  mrcflem  15098  mrcval  15102  isacs2  15145  acsfiel  15146  ipoval  15986  fpwipodrs  15996  ipodrsima  15997  mreclatBAD  16019  slwispgp  16833  pgpssslw  16836  lsmss1b  16887  lsmss2b  16889  cntzcmnss  17051  gsumzres  17116  lspf  17818  lspval  17819  lbsextlem1  18002  lbsextlem3  18004  lbsextlem4  18005  aspval  18175  mplsubglem  18291  mpllsslem  18292  mplsubglemOLD  18293  mpllsslemOLD  18294  basis2  19622  eltg2  19629  clsval  19708  clscld  19718  clsval2  19721  ntrcls0  19747  isnei  19774  neiint  19775  neips  19784  opnneissb  19785  opnssneib  19786  neindisj2  19794  innei  19796  neiptoptop  19802  neiptopnei  19803  neitr  19851  restcls  19852  cnpimaex  19927  cnprest2  19961  regsep  20005  nrmsep3  20026  nrmsep  20028  regsep2  20047  tgcmp  20071  uncmp  20073  bwth  20080  1stcfb  20115  1stcrest  20123  2ndcctbss  20125  1stcelcls  20131  lly1stc  20166  ssref  20182  refref  20183  comppfsc  20202  xkoopn  20259  neitx  20277  txcnp  20290  txcmplem1  20311  kqnrmlem1  20413  kqnrmlem2  20414  nrmhmph  20464  fbssfi  20507  opnfbas  20512  fbasfip  20538  fbunfip  20539  fgss2  20544  fgcl  20548  supfil  20565  isufil2  20578  filssufilg  20581  ssufl  20588  ufileu  20589  elfm3  20620  fmfnfm  20628  ufldom  20632  fbflim2  20647  flfneii  20662  flftg  20666  txflf  20676  supnfcls  20690  fclscf  20695  fclsfnflim  20697  flimfnfcls  20698  alexsubALTlem2  20717  alexsubALTlem3  20718  alexsubALTlem4  20719  alexsubALT  20720  tsmsfbas  20795  tsmsresOLD  20814  tsmsres  20815  tsmsf1o  20816  tsmsxplem1  20824  tsmsxp  20826  ustssel  20877  ustincl  20879  ustdiag  20880  ustinvel  20881  ustexhalf  20882  ust0  20891  elutop  20905  ustuqtop4  20916  cfiluexsm  20962  cfiluweak  20967  blssps  21096  blss  21097  metss  21180  metrest  21196  metcnp3  21212  metnrmlem3  21534  lebnumlem3  21632  lebnum  21633  ellimc3  22452  lhop1lem  22583  dchrelbas  23712  avril1  25376  resgrprn  25483  spanval  26452  spancl  26455  shsval2i  26506  omlsi  26523  ococin  26527  chsupsn  26532  pjoml  26555  shs00i  26569  chj00i  26606  chsscon3  26619  chlejb1  26631  chnle  26633  pjoml2  26730  pjoml3  26731  lecm  26736  stcltr1i  27394  mdbr  27414  dmdmd  27420  dmdi  27422  dmdbr3  27425  dmdbr4  27426  mdsl1i  27441  mdslmd1lem3  27447  mdslmd1lem4  27448  csmdsymi  27454  hatomic  27480  chrelat2  27490  atord  27508  atcvat4i  27517  reff  28080  cmpcref  28091  sigagenval  28373  dmsigagen  28377  sigagenss  28382  carsgmon  28525  carsgclctunlem2  28530  kur14lem9  28925  mclsssvlem  29189  mclsind  29197  wrecseq123  29580  wfrlem1  29586  wfrlem4  29589  wfrlem15  29600  frrlem1  29630  frrlem4  29633  frrlem5e  29638  frrlem11  29642  imagesset  29834  altopthsn  29842  mblfinlem3  30296  fnessref  30418  refssfne  30419  topjoin  30426  neifg  30432  totbndss  30516  heibor1lem  30548  unichnidl  30671  ispridl  30674  maxidlmax  30683  igenval  30701  igenidl  30703  igenmin  30704  igenval2  30706  nacsfix  30887  mzpcompact2  30927  rgspnval  31361  rgspncl  31362  rgspnmin  31364  ssrecnpr  31432  islptre  31867  bnj1286  34495  bnj1452  34528  bj-snglex  34951  lsatcmp  35144  lcvexchlem4  35178  lcvexchlem5  35179  pclvalN  36030  pclclN  36031  elpcliN  36033  docaclN  37267  dihglb2  37485  doch2val2  37507  dochocss  37509  dochexmidlem7  37609  lpolconN  37630  mapdval  37771  superficl  38184  superuncl  38185  dfrcl2  38214  dfrtrcl3  38235  brtrclfv2  38261
  Copyright terms: Public domain W3C validator