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

Theorem sseq2 3466
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 3451 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 32 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3451 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 32 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 574 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3459 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 638 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 274 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1455    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  sseq12  3467  sseq2i  3469  sseq2d  3472  syl5sseq  3492  nssne1  3500  psseq2  3533  sseq0  3778  un00  3812  disjpss  3827  pweq  3966  ssintab  4265  ssintub  4266  intmin  4268  treq  4517  sseliALT  4550  ssexg  4563  intabs  4578  ordunidif  5490  ordssun  5541  fununi  5671  feq3  5734  ssimaexg  5954  iunpw  6632  tfindsg  6714  limomss  6724  findsg  6747  funcnvuni  6773  frxp  6933  wrecseq123  7055  wfrlem1  7061  wfrlem4  7065  wfrlem15  7076  onfununi  7086  oawordeu  7282  oawordexr  7283  nnawordex  7364  ereq1  7396  xpider  7460  domeng  7609  sbthlem4  7711  sbthlem5  7712  domssex  7759  finsschain  7907  dffi2  7963  dffi3  7971  hartogslem1  8083  inf3lema  8155  cantnflem1  8220  tz9.1  8239  tz9.1c  8240  tctr  8250  tcmin  8251  tcrank  8381  scottex  8382  cardlim  8432  infxpenlem  8470  infxpenc2  8479  isinfcard  8549  alephinit  8552  alephval3  8567  dfac3  8578  cflem  8702  cfval  8703  cflecard  8709  cfsuc  8713  cff1  8714  cfflb  8715  cflim2  8719  isf32lem2  8810  fin1a2lem13  8868  ac7g  8930  ttukeylem5  8969  ttukeylem7  8971  pwcfsdom  9034  pwfseqlem5  9114  pwfseq  9115  gch2  9126  winalim  9146  wunex  9190  wuncss  9196  eltskg  9201  eltsk2g  9202  gruina  9269  grur1a  9270  axgroth6  9279  swrdnd2  12826  trcleq2lem  13104  dfrtrcl2  13174  fprodss  14051  mrcflem  15561  mrcval  15565  isacs2  15608  acsfiel  15609  ipoval  16449  fpwipodrs  16459  ipodrsima  16460  mreclatBAD  16482  slwispgp  17312  pgpssslw  17315  lsmss1b  17366  lsmss2b  17368  cntzcmnss  17530  gsumzres  17592  lspf  18246  lspval  18247  lbsextlem1  18430  lbsextlem3  18432  lbsextlem4  18433  aspval  18601  mplsubglem  18707  mpllsslem  18708  basis2  20015  eltg2  20022  clsval  20101  clscld  20111  clsval2  20114  ntrcls0  20141  isnei  20168  neiint  20169  neips  20178  opnneissb  20179  opnssneib  20180  neindisj2  20188  innei  20190  neiptoptop  20196  neiptopnei  20197  neitr  20245  restcls  20246  cnpimaex  20321  cnprest2  20355  regsep  20399  nrmsep3  20420  nrmsep  20422  regsep2  20441  tgcmp  20465  uncmp  20467  bwth  20474  1stcfb  20509  1stcrest  20517  2ndcctbss  20519  1stcelcls  20525  lly1stc  20560  ssref  20576  refref  20577  comppfsc  20596  xkoopn  20653  neitx  20671  txcnp  20684  txcmplem1  20705  kqnrmlem1  20807  kqnrmlem2  20808  nrmhmph  20858  fbssfi  20901  opnfbas  20906  fbasfip  20932  fbunfip  20933  fgss2  20938  fgcl  20942  supfil  20959  isufil2  20972  filssufilg  20975  ssufl  20982  ufileu  20983  elfm3  21014  fmfnfm  21022  ufldom  21026  fbflim2  21041  flfneii  21056  flftg  21060  txflf  21070  supnfcls  21084  fclscf  21089  fclsfnflim  21091  flimfnfcls  21092  alexsubALTlem2  21112  alexsubALTlem3  21113  alexsubALTlem4  21114  alexsubALT  21115  tsmsfbas  21191  tsmsres  21207  tsmsf1o  21208  tsmsxplem1  21216  tsmsxp  21218  ustssel  21269  ustincl  21271  ustdiag  21272  ustinvel  21273  ustexhalf  21274  ust0  21283  elutop  21297  ustuqtop4  21308  cfiluexsm  21354  cfiluweak  21359  blssps  21488  blss  21489  metss  21572  metrest  21588  metcnp3  21604  metnrmlem3  21927  metnrmlem3OLD  21942  lebnumlem3  22040  lebnumlem3OLD  22043  lebnum  22044  ellimc3  22883  lhop1lem  23014  dchrelbas  24213  avril1  25949  resgrprn  26057  spanval  27035  spancl  27038  shsval2i  27089  omlsi  27106  ococin  27110  chsupsn  27115  pjoml  27138  shs00i  27152  chj00i  27189  chsscon3  27202  chlejb1  27214  chnle  27216  pjoml2  27313  pjoml3  27314  lecm  27319  stcltr1i  27976  mdbr  27996  dmdmd  28002  dmdi  28004  dmdbr3  28007  dmdbr4  28008  mdsl1i  28023  mdslmd1lem3  28029  mdslmd1lem4  28030  csmdsymi  28036  hatomic  28062  chrelat2  28072  atord  28090  atcvat4i  28099  fz1nntr  28427  reff  28715  cmpcref  28726  sigagenval  29011  dmsigagen  29015  sigagenss  29020  ldsysgenld  29031  ldgenpisyslem1  29034  ldgenpisyslem2  29035  dynkin  29038  carsgmon  29195  carsgclctunlem2  29200  bnj1286  29877  bnj1452  29910  kur14lem9  29986  mclsssvlem  30249  mclsind  30257  frrlem1  30563  frrlem4  30566  frrlem5e  30571  frrlem11  30575  imagesset  30769  altopthsn  30777  fnessref  31062  refssfne  31063  topjoin  31070  neifg  31076  bj-snglex  31612  relowlssretop  31811  relowlpssretop  31812  finxpreclem3  31830  poimirlem29  32014  poimir  32018  mblfinlem3  32024  totbndss  32154  heibor1lem  32186  unichnidl  32309  ispridl  32312  maxidlmax  32321  igenval  32339  igenidl  32341  igenmin  32342  igenval2  32344  lsatcmp  32614  lcvexchlem4  32648  lcvexchlem5  32649  pclvalN  33500  pclclN  33501  elpcliN  33503  docaclN  34737  dihglb2  34955  doch2val2  34977  dochocss  34979  dochexmidlem7  35079  lpolconN  35100  mapdval  35241  nacsfix  35599  mzpcompact2  35639  rgspnval  36079  rgspncl  36080  rgspnmin  36082  superficl  36216  superuncl  36217  cleq2lem  36259  clcnvlem  36275  dfrtrcl3  36370  ssrecnpr  36700  founiiun  37484  founiiun0  37503  islptre  37737  salgenval  38220  salgenn0  38228  salgencl  38229  sssalgen  38232  salgenss  38233  salgenuni  38234  issalgend  38235  dfsalgen2  38238  salgencntex  38240  iunopeqop  39045  upgredgpr  39280  dfnbgr3  39458  nbupgr  39462  nbumgrvtx  39464  nbgr2vtx1edg  39468  nbuhgr2vtx1edgb  39470  cusgrexi  39557  1wlkvtxiedg  39687  upgr11wlkdlem2  39861  1pthon2v-av  39868  1pthon2ve  39869  cusconngr  39932
  Copyright terms: Public domain W3C validator