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

Theorem sseq2 3492
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 3477 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 32 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3477 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 32 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 568 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3485 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 632 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 269 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  sseq12  3493  sseq2i  3495  sseq2d  3498  syl5sseq  3518  nssne1  3526  psseq2  3559  sseq0  3800  un00  3834  disjpss  3849  pweq  3988  ssintab  4275  ssintub  4276  intmin  4278  treq  4526  sseliALT  4558  ssexg  4571  intabs  4586  ordunidif  5490  ordssun  5541  fununi  5667  feq3  5730  ssimaexg  5947  iunpw  6619  tfindsg  6701  limomss  6711  findsg  6734  funcnvuni  6760  frxp  6917  wrecseq123  7037  wfrlem1  7043  wfrlem4  7047  wfrlem15  7058  onfununi  7068  oawordeu  7264  oawordexr  7265  nnawordex  7346  ereq1  7378  xpider  7442  domeng  7591  sbthlem4  7691  sbthlem5  7692  domssex  7739  finsschain  7887  dffi2  7943  dffi3  7951  hartogslem1  8057  inf3lema  8129  cantnflem1  8193  tz9.1  8212  tz9.1c  8213  tctr  8223  tcmin  8224  tcrank  8354  scottex  8355  cardlim  8405  infxpenlem  8443  infxpenc2  8451  isinfcard  8521  alephinit  8524  alephval3  8539  dfac3  8550  cflem  8674  cfval  8675  cflecard  8681  cfsuc  8685  cff1  8686  cfflb  8687  cflim2  8691  isf32lem2  8782  fin1a2lem13  8840  ac7g  8902  ttukeylem5  8941  ttukeylem7  8943  pwcfsdom  9006  pwfseqlem5  9087  pwfseq  9088  gch2  9099  winalim  9119  wunex  9163  wuncss  9169  eltskg  9174  eltsk2g  9175  gruina  9242  grur1a  9243  axgroth6  9252  swrdnd2  12774  trcleq2lem  13034  dfrtrcl2  13104  fprodss  13980  mrcflem  15463  mrcval  15467  isacs2  15510  acsfiel  15511  ipoval  16351  fpwipodrs  16361  ipodrsima  16362  mreclatBAD  16384  slwispgp  17198  pgpssslw  17201  lsmss1b  17252  lsmss2b  17254  cntzcmnss  17416  gsumzres  17478  lspf  18132  lspval  18133  lbsextlem1  18316  lbsextlem3  18318  lbsextlem4  18319  aspval  18487  mplsubglem  18593  mpllsslem  18594  basis2  19897  eltg2  19904  clsval  19983  clscld  19993  clsval2  19996  ntrcls0  20023  isnei  20050  neiint  20051  neips  20060  opnneissb  20061  opnssneib  20062  neindisj2  20070  innei  20072  neiptoptop  20078  neiptopnei  20079  neitr  20127  restcls  20128  cnpimaex  20203  cnprest2  20237  regsep  20281  nrmsep3  20302  nrmsep  20304  regsep2  20323  tgcmp  20347  uncmp  20349  bwth  20356  1stcfb  20391  1stcrest  20399  2ndcctbss  20401  1stcelcls  20407  lly1stc  20442  ssref  20458  refref  20459  comppfsc  20478  xkoopn  20535  neitx  20553  txcnp  20566  txcmplem1  20587  kqnrmlem1  20689  kqnrmlem2  20690  nrmhmph  20740  fbssfi  20783  opnfbas  20788  fbasfip  20814  fbunfip  20815  fgss2  20820  fgcl  20824  supfil  20841  isufil2  20854  filssufilg  20857  ssufl  20864  ufileu  20865  elfm3  20896  fmfnfm  20904  ufldom  20908  fbflim2  20923  flfneii  20938  flftg  20942  txflf  20952  supnfcls  20966  fclscf  20971  fclsfnflim  20973  flimfnfcls  20974  alexsubALTlem2  20994  alexsubALTlem3  20995  alexsubALTlem4  20996  alexsubALT  20997  tsmsfbas  21073  tsmsres  21089  tsmsf1o  21090  tsmsxplem1  21098  tsmsxp  21100  ustssel  21151  ustincl  21153  ustdiag  21154  ustinvel  21155  ustexhalf  21156  ust0  21165  elutop  21179  ustuqtop4  21190  cfiluexsm  21236  cfiluweak  21241  blssps  21370  blss  21371  metss  21454  metrest  21470  metcnp3  21486  metnrmlem3  21789  lebnumlem3  21887  lebnum  21888  ellimc3  22711  lhop1lem  22842  dchrelbas  24027  avril1  25745  resgrprn  25853  spanval  26821  spancl  26824  shsval2i  26875  omlsi  26892  ococin  26896  chsupsn  26901  pjoml  26924  shs00i  26938  chj00i  26975  chsscon3  26988  chlejb1  27000  chnle  27002  pjoml2  27099  pjoml3  27100  lecm  27105  stcltr1i  27762  mdbr  27782  dmdmd  27788  dmdi  27790  dmdbr3  27793  dmdbr4  27794  mdsl1i  27809  mdslmd1lem3  27815  mdslmd1lem4  27816  csmdsymi  27822  hatomic  27848  chrelat2  27858  atord  27876  atcvat4i  27885  fz1nntr  28214  reff  28505  cmpcref  28516  sigagenval  28801  dmsigagen  28805  sigagenss  28810  ldsysgenld  28821  ldgenpisyslem1  28824  ldgenpisyslem2  28825  dynkin  28828  carsgmon  28975  carsgclctunlem2  28980  bnj1286  29616  bnj1452  29649  kur14lem9  29725  mclsssvlem  29988  mclsind  29996  frrlem1  30301  frrlem4  30304  frrlem5e  30309  frrlem11  30313  imagesset  30505  altopthsn  30513  fnessref  30798  refssfne  30799  topjoin  30806  neifg  30812  bj-snglex  31316  relowlssretop  31500  relowlpssretop  31501  poimirlem29  31673  poimir  31677  mblfinlem3  31683  totbndss  31813  heibor1lem  31845  unichnidl  31968  ispridl  31971  maxidlmax  31980  igenval  31998  igenidl  32000  igenmin  32001  igenval2  32003  lsatcmp  32278  lcvexchlem4  32312  lcvexchlem5  32313  pclvalN  33164  pclclN  33165  elpcliN  33167  docaclN  34401  dihglb2  34619  doch2val2  34641  dochocss  34643  dochexmidlem7  34743  lpolconN  34764  mapdval  34905  nacsfix  35263  mzpcompact2  35303  rgspnval  35733  rgspncl  35734  rgspnmin  35736  superficl  35870  superuncl  35871  dfrcl2  35905  brtrclfv2  35958  dfrtrcl3  35964  ssrecnpr  36293  founiiun  37069  founiiun0  37088  islptre  37271
  Copyright terms: Public domain W3C validator