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

Theorem sseq2 3383
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 3368 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 31 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3368 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 31 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 566 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3376 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 628 . 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 1369    C_ wss 3333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3340  df-ss 3347
This theorem is referenced by:  sseq12  3384  sseq2i  3386  sseq2d  3389  syl5sseq  3409  nssne1  3417  psseq2  3449  sseq0  3674  un00  3719  disjpss  3734  pweq  3868  ssintab  4150  ssintub  4151  intmin  4153  treq  4396  sseliALT  4428  ssexg  4443  intabs  4458  ordunidif  4772  ordssun  4823  fununi  5489  feq3  5549  ssimaexg  5762  iunpw  6395  tfindsg  6476  limomss  6486  findsg  6508  funcnvuni  6535  frxp  6687  onfununi  6807  oawordeu  6999  oawordexr  7000  nnawordex  7081  ereq1  7113  xpider  7176  domeng  7329  sbthlem4  7429  sbthlem5  7430  domssex  7477  finsschain  7623  dffi2  7678  dffi3  7686  hartogslem1  7761  inf3lema  7835  cantnflem1  7902  cantnflem1OLD  7925  tz9.1  7954  tz9.1c  7955  tctr  7965  tcmin  7966  tcrank  8096  scottex  8097  cardlim  8147  infxpenlem  8185  infxpenc2  8193  infxpenc2OLD  8197  isinfcard  8267  alephinit  8270  alephval3  8285  dfac3  8296  cflem  8420  cfval  8421  cflecard  8427  cfsuc  8431  cff1  8432  cfflb  8433  cflim2  8437  isf32lem2  8528  fin1a2lem13  8586  ac7g  8648  ttukeylem5  8687  ttukeylem7  8689  pwcfsdom  8752  pwfseqlem5  8835  pwfseq  8836  gch2  8847  winalim  8867  wunex  8911  wuncss  8917  eltskg  8922  eltsk2g  8923  gruina  8990  grur1a  8991  axgroth6  9000  swrdvalodm2  12338  swrdvalodm  12339  mrcflem  14549  mrcval  14553  isacs2  14596  acsfiel  14597  ipoval  15329  fpwipodrs  15339  ipodrsima  15340  mreclatBAD  15362  slwispgp  16115  pgpssslw  16118  lsmss1b  16169  lsmss2b  16171  cntzcmnss  16330  gsumzres  16393  lspf  17060  lspval  17061  lbsextlem1  17244  lbsextlem3  17246  lbsextlem4  17247  aspval  17404  mplsubglem  17515  mpllsslem  17516  mplsubglemOLD  17517  mpllsslemOLD  17518  basis2  18561  eltg2  18568  clsval  18646  clscld  18656  clsval2  18659  ntrcls0  18685  isnei  18712  neiint  18713  neips  18722  opnneissb  18723  opnssneib  18724  neindisj2  18732  innei  18734  neiptoptop  18740  neiptopnei  18741  neitr  18789  restcls  18790  cnpimaex  18865  cnprest2  18899  regsep  18943  nrmsep3  18964  nrmsep  18966  regsep2  18985  tgcmp  19009  uncmp  19011  bwth  19018  bwthOLD  19019  1stcfb  19054  1stcrest  19062  2ndcctbss  19064  1stcelcls  19070  lly1stc  19105  xkoopn  19167  neitx  19185  txcnp  19198  txcmplem1  19219  kqnrmlem1  19321  kqnrmlem2  19322  nrmhmph  19372  fbssfi  19415  opnfbas  19420  fbasfip  19446  fbunfip  19447  fgss2  19452  fgcl  19456  supfil  19473  isufil2  19486  filssufilg  19489  ssufl  19496  ufileu  19497  elfm3  19528  fmfnfm  19536  ufldom  19540  fbflim2  19555  flfneii  19570  flftg  19574  txflf  19584  supnfcls  19598  fclscf  19603  fclsfnflim  19605  flimfnfcls  19606  alexsubALTlem2  19625  alexsubALTlem3  19626  alexsubALTlem4  19627  alexsubALT  19628  tsmsfbas  19703  tsmsresOLD  19722  tsmsres  19723  tsmsf1o  19724  tsmsxplem1  19732  tsmsxp  19734  ustssel  19785  ustincl  19787  ustdiag  19788  ustinvel  19789  ustexhalf  19790  ust0  19799  elutop  19813  ustuqtop4  19824  cfiluexsm  19870  cfiluweak  19875  blssps  20004  blss  20005  metss  20088  metrest  20104  metcnp3  20120  metnrmlem3  20442  lebnumlem3  20540  lebnum  20541  ellimc3  21359  lhop1lem  21490  dchrelbas  22580  avril1  23661  resgrprn  23772  spanval  24741  spancl  24744  shsval2i  24795  omlsi  24812  ococin  24816  chsupsn  24821  pjoml  24844  shs00i  24858  chj00i  24895  chsscon3  24908  chlejb1  24920  chnle  24922  pjoml2  25019  pjoml3  25020  lecm  25025  stcltr1i  25683  mdbr  25703  dmdmd  25709  dmdi  25711  dmdbr3  25714  dmdbr4  25715  mdsl1i  25730  mdslmd1lem3  25736  mdslmd1lem4  25737  csmdsymi  25743  hatomic  25769  chrelat2  25779  atord  25797  atcvat4i  25806  sigagenval  26588  dmsigagen  26592  sigagenss  26597  kur14lem9  27107  dfrtrcl2  27355  fprodss  27466  wrecseq123  27723  wfrlem1  27729  wfrlem4  27732  wfrlem15  27743  frrlem1  27773  frrlem4  27776  frrlem5e  27781  frrlem11  27785  imagesset  27989  altopthsn  27997  mblfinlem3  28435  ssref  28560  refref  28562  fnessref  28570  refssfne  28571  comppfsc  28584  topjoin  28591  neifg  28597  totbndss  28681  heibor1lem  28713  unichnidl  28836  ispridl  28839  maxidlmax  28848  igenval  28866  igenidl  28868  igenmin  28869  igenval2  28871  nacsfix  29053  mzpcompact2  29094  rgspnval  29530  rgspncl  29531  rgspnmin  29533  ssrecnpr  29599  bnj1286  32015  bnj1452  32048  bj-snglex  32471  lsatcmp  32653  lcvexchlem4  32687  lcvexchlem5  32688  pclvalN  33539  pclclN  33540  elpcliN  33542  docaclN  34774  dihglb2  34992  doch2val2  35014  dochocss  35016  dochexmidlem7  35116  lpolconN  35137  mapdval  35278
  Copyright terms: Public domain W3C validator