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

Theorem sseq2 3366
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 3351 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 31 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3351 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 31 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 561 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3359 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 621 . 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 369    = wceq 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  sseq12  3367  sseq2i  3369  sseq2d  3372  syl5sseq  3392  nssne1  3400  psseq2  3432  sseq0  3657  un00  3702  disjpss  3717  pweq  3851  ssintab  4133  ssintub  4134  intmin  4136  treq  4379  sseliALT  4411  ssexg  4426  intabs  4441  ordunidif  4754  ordssun  4805  fununi  5472  feq3  5532  ssimaexg  5745  iunpw  6379  tfindsg  6460  limomss  6470  findsg  6492  funcnvuni  6519  frxp  6671  onfununi  6788  oawordeu  6982  oawordexr  6983  nnawordex  7064  ereq1  7096  xpider  7159  domeng  7312  sbthlem4  7412  sbthlem5  7413  domssex  7460  finsschain  7606  dffi2  7661  dffi3  7669  hartogslem1  7744  inf3lema  7818  cantnflem1  7885  cantnflem1OLD  7908  tz9.1  7937  tz9.1c  7938  tctr  7948  tcmin  7949  tcrank  8079  scottex  8080  cardlim  8130  infxpenlem  8168  infxpenc2  8176  infxpenc2OLD  8180  isinfcard  8250  alephinit  8253  alephval3  8268  dfac3  8279  cflem  8403  cfval  8404  cflecard  8410  cfsuc  8414  cff1  8415  cfflb  8416  cflim2  8420  isf32lem2  8511  fin1a2lem13  8569  ac7g  8631  ttukeylem5  8670  ttukeylem7  8672  pwcfsdom  8735  pwfseqlem5  8817  pwfseq  8818  gch2  8829  winalim  8849  wunex  8893  wuncss  8899  eltskg  8904  eltsk2g  8905  gruina  8972  grur1a  8973  axgroth6  8982  swrdvalodm2  12316  swrdvalodm  12317  mrcflem  14526  mrcval  14530  isacs2  14573  acsfiel  14574  ipoval  15306  fpwipodrs  15316  ipodrsima  15317  mreclatBAD  15339  slwispgp  16089  pgpssslw  16092  lsmss1b  16143  lsmss2b  16145  cntzcmnss  16304  gsumzres  16367  lspf  16976  lspval  16977  lbsextlem1  17160  lbsextlem3  17162  lbsextlem4  17163  aspval  17320  mplsubglem  17443  mpllsslem  17444  mplsubglemOLD  17445  mpllsslemOLD  17446  basis2  18397  eltg2  18404  clsval  18482  clscld  18492  clsval2  18495  ntrcls0  18521  isnei  18548  neiint  18549  neips  18558  opnneissb  18559  opnssneib  18560  neindisj2  18568  innei  18570  neiptoptop  18576  neiptopnei  18577  neitr  18625  restcls  18626  cnpimaex  18701  cnprest2  18735  regsep  18779  nrmsep3  18800  nrmsep  18802  regsep2  18821  tgcmp  18845  uncmp  18847  bwth  18854  bwthOLD  18855  1stcfb  18890  1stcrest  18898  2ndcctbss  18900  1stcelcls  18906  lly1stc  18941  xkoopn  19003  neitx  19021  txcnp  19034  txcmplem1  19055  kqnrmlem1  19157  kqnrmlem2  19158  nrmhmph  19208  fbssfi  19251  opnfbas  19256  fbasfip  19282  fbunfip  19283  fgss2  19288  fgcl  19292  supfil  19309  isufil2  19322  filssufilg  19325  ssufl  19332  ufileu  19333  elfm3  19364  fmfnfm  19372  ufldom  19376  fbflim2  19391  flfneii  19406  flftg  19410  txflf  19420  supnfcls  19434  fclscf  19439  fclsfnflim  19441  flimfnfcls  19442  alexsubALTlem2  19461  alexsubALTlem3  19462  alexsubALTlem4  19463  alexsubALT  19464  tsmsfbas  19539  tsmsresOLD  19558  tsmsres  19559  tsmsf1o  19560  tsmsxplem1  19568  tsmsxp  19570  ustssel  19621  ustincl  19623  ustdiag  19624  ustinvel  19625  ustexhalf  19626  ust0  19635  elutop  19649  ustuqtop4  19660  cfiluexsm  19706  cfiluweak  19711  blssps  19840  blss  19841  metss  19924  metrest  19940  metcnp3  19956  metnrmlem3  20278  lebnumlem3  20376  lebnum  20377  ellimc3  21195  lhop1lem  21326  dchrelbas  22459  avril1  23478  resgrprn  23589  spanval  24558  spancl  24561  shsval2i  24612  omlsi  24629  ococin  24633  chsupsn  24638  pjoml  24661  shs00i  24675  chj00i  24712  chsscon3  24725  chlejb1  24737  chnle  24739  pjoml2  24836  pjoml3  24837  lecm  24842  stcltr1i  25500  mdbr  25520  dmdmd  25526  dmdi  25528  dmdbr3  25531  dmdbr4  25532  mdsl1i  25547  mdslmd1lem3  25553  mdslmd1lem4  25554  csmdsymi  25560  hatomic  25586  chrelat2  25596  atord  25614  atcvat4i  25623  sigagenval  26436  dmsigagen  26440  sigagenss  26445  kur14lem9  26949  dfrtrcl2  27196  fprodss  27307  wrecseq123  27564  wfrlem1  27570  wfrlem4  27573  wfrlem15  27584  frrlem1  27614  frrlem4  27617  frrlem5e  27622  frrlem11  27626  imagesset  27830  altopthsn  27838  mblfinlem3  28271  ssref  28396  refref  28398  fnessref  28406  refssfne  28407  comppfsc  28420  topjoin  28427  neifg  28433  totbndss  28517  heibor1lem  28549  unichnidl  28672  ispridl  28675  maxidlmax  28684  igenval  28702  igenidl  28704  igenmin  28705  igenval2  28707  nacsfix  28890  mzpcompact2  28931  rgspnval  29367  rgspncl  29368  rgspnmin  29370  ssrecnpr  29436  bnj1286  31709  bnj1452  31742  bj-snglex  32046  lsatcmp  32218  lcvexchlem4  32252  lcvexchlem5  32253  pclvalN  33104  pclclN  33105  elpcliN  33107  docaclN  34339  dihglb2  34557  doch2val2  34579  dochocss  34581  dochexmidlem7  34681  lpolconN  34702  mapdval  34843
  Copyright terms: Public domain W3C validator