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

Theorem sseq2 3526
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 3511 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 31 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3511 . . . 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 3519 . 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 1379    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  sseq12  3527  sseq2i  3529  sseq2d  3532  syl5sseq  3552  nssne1  3560  psseq2  3592  sseq0  3817  un00  3862  disjpss  3877  pweq  4013  ssintab  4299  ssintub  4300  intmin  4302  treq  4546  sseliALT  4578  ssexg  4593  intabs  4608  ordunidif  4926  ordssun  4977  fununi  5652  feq3  5713  ssimaexg  5931  iunpw  6592  tfindsg  6673  limomss  6683  findsg  6705  funcnvuni  6734  frxp  6890  onfununi  7009  oawordeu  7201  oawordexr  7202  nnawordex  7283  ereq1  7315  xpider  7379  domeng  7527  sbthlem4  7627  sbthlem5  7628  domssex  7675  finsschain  7823  dffi2  7879  dffi3  7887  hartogslem1  7963  inf3lema  8037  cantnflem1  8104  cantnflem1OLD  8127  tz9.1  8156  tz9.1c  8157  tctr  8167  tcmin  8168  tcrank  8298  scottex  8299  cardlim  8349  infxpenlem  8387  infxpenc2  8395  infxpenc2OLD  8399  isinfcard  8469  alephinit  8472  alephval3  8487  dfac3  8498  cflem  8622  cfval  8623  cflecard  8629  cfsuc  8633  cff1  8634  cfflb  8635  cflim2  8639  isf32lem2  8730  fin1a2lem13  8788  ac7g  8850  ttukeylem5  8889  ttukeylem7  8891  pwcfsdom  8954  pwfseqlem5  9037  pwfseq  9038  gch2  9049  winalim  9069  wunex  9113  wuncss  9119  eltskg  9124  eltsk2g  9125  gruina  9192  grur1a  9193  axgroth6  9202  swrdvalodm2  12623  swrdvalodm  12624  mrcflem  14857  mrcval  14861  isacs2  14904  acsfiel  14905  ipoval  15637  fpwipodrs  15647  ipodrsima  15648  mreclatBAD  15670  slwispgp  16427  pgpssslw  16430  lsmss1b  16481  lsmss2b  16483  cntzcmnss  16642  gsumzres  16705  lspf  17403  lspval  17404  lbsextlem1  17587  lbsextlem3  17589  lbsextlem4  17590  aspval  17748  mplsubglem  17864  mpllsslem  17865  mplsubglemOLD  17866  mpllsslemOLD  17867  basis2  19219  eltg2  19226  clsval  19304  clscld  19314  clsval2  19317  ntrcls0  19343  isnei  19370  neiint  19371  neips  19380  opnneissb  19381  opnssneib  19382  neindisj2  19390  innei  19392  neiptoptop  19398  neiptopnei  19399  neitr  19447  restcls  19448  cnpimaex  19523  cnprest2  19557  regsep  19601  nrmsep3  19622  nrmsep  19624  regsep2  19643  tgcmp  19667  uncmp  19669  bwth  19676  bwthOLD  19677  1stcfb  19712  1stcrest  19720  2ndcctbss  19722  1stcelcls  19728  lly1stc  19763  xkoopn  19825  neitx  19843  txcnp  19856  txcmplem1  19877  kqnrmlem1  19979  kqnrmlem2  19980  nrmhmph  20030  fbssfi  20073  opnfbas  20078  fbasfip  20104  fbunfip  20105  fgss2  20110  fgcl  20114  supfil  20131  isufil2  20144  filssufilg  20147  ssufl  20154  ufileu  20155  elfm3  20186  fmfnfm  20194  ufldom  20198  fbflim2  20213  flfneii  20228  flftg  20232  txflf  20242  supnfcls  20256  fclscf  20261  fclsfnflim  20263  flimfnfcls  20264  alexsubALTlem2  20283  alexsubALTlem3  20284  alexsubALTlem4  20285  alexsubALT  20286  tsmsfbas  20361  tsmsresOLD  20380  tsmsres  20381  tsmsf1o  20382  tsmsxplem1  20390  tsmsxp  20392  ustssel  20443  ustincl  20445  ustdiag  20446  ustinvel  20447  ustexhalf  20448  ust0  20457  elutop  20471  ustuqtop4  20482  cfiluexsm  20528  cfiluweak  20533  blssps  20662  blss  20663  metss  20746  metrest  20762  metcnp3  20778  metnrmlem3  21100  lebnumlem3  21198  lebnum  21199  ellimc3  22018  lhop1lem  22149  dchrelbas  23239  avril1  24847  resgrprn  24958  spanval  25927  spancl  25930  shsval2i  25981  omlsi  25998  ococin  26002  chsupsn  26007  pjoml  26030  shs00i  26044  chj00i  26081  chsscon3  26094  chlejb1  26106  chnle  26108  pjoml2  26205  pjoml3  26206  lecm  26211  stcltr1i  26869  mdbr  26889  dmdmd  26895  dmdi  26897  dmdbr3  26900  dmdbr4  26901  mdsl1i  26916  mdslmd1lem3  26922  mdslmd1lem4  26923  csmdsymi  26929  hatomic  26955  chrelat2  26965  atord  26983  atcvat4i  26992  sigagenval  27780  dmsigagen  27784  sigagenss  27789  kur14lem9  28298  dfrtrcl2  28546  fprodss  28657  wrecseq123  28914  wfrlem1  28920  wfrlem4  28923  wfrlem15  28934  frrlem1  28964  frrlem4  28967  frrlem5e  28972  frrlem11  28976  imagesset  29180  altopthsn  29188  mblfinlem3  29630  ssref  29755  refref  29757  fnessref  29765  refssfne  29766  comppfsc  29779  topjoin  29786  neifg  29792  totbndss  29876  heibor1lem  29908  unichnidl  30031  ispridl  30034  maxidlmax  30043  igenval  30061  igenidl  30063  igenmin  30064  igenval2  30066  nacsfix  30248  mzpcompact2  30289  rgspnval  30722  rgspncl  30723  rgspnmin  30725  ssrecnpr  30791  islptre  31161  bnj1286  33154  bnj1452  33187  bj-snglex  33612  lsatcmp  33800  lcvexchlem4  33834  lcvexchlem5  33835  pclvalN  34686  pclclN  34687  elpcliN  34689  docaclN  35921  dihglb2  36139  doch2val2  36161  dochocss  36163  dochexmidlem7  36263  lpolconN  36284  mapdval  36425  superficl  36772  superuncl  36773  trclub  36794  trclubg  36795
  Copyright terms: Public domain W3C validator