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

Theorem sseq2 3315
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 3300 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 29 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3300 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 29 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 550 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3308 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 610 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 258 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    C_ wss 3265
This theorem is referenced by:  sseq12  3316  sseq2i  3318  sseq2d  3321  syl5sseq  3341  nssne1  3349  psseq2  3380  sseq0  3604  un00  3608  disjpss  3623  pweq  3747  ssintab  4011  ssintub  4012  intmin  4014  treq  4251  ssexg  4292  intabs  4304  ordunidif  4572  ordssun  4623  iunpw  4701  tfindsg  4782  limomss  4792  findsg  4814  fununi  5459  funcnvuni  5460  feq3  5520  ssimaexg  5730  frxp  6394  onfununi  6541  oawordeu  6736  oawordexr  6737  nnawordex  6818  ereq1  6850  xpider  6913  domeng  7060  sbthlem4  7158  sbthlem5  7159  domssex  7206  finsschain  7350  dffi2  7365  dffi3  7373  hartogslem1  7446  inf3lema  7514  cantnflem1  7580  tz9.1  7600  tz9.1c  7601  tctr  7614  tcmin  7615  tcrank  7743  scottex  7744  cardlim  7794  infxpenlem  7830  infxpenc2  7838  isinfcard  7908  alephinit  7911  alephval3  7926  dfac3  7937  cflem  8061  cfval  8062  cflecard  8068  cfsuc  8072  cff1  8073  cfflb  8074  cflim2  8078  isf32lem2  8169  fin1a2lem13  8227  ac7g  8289  ttukeylem5  8328  ttukeylem7  8330  pwcfsdom  8393  pwfseqlem5  8473  pwfseq  8474  gch2  8489  winalim  8505  wunex  8549  wuncss  8555  eltskg  8560  eltsk2g  8561  gruina  8628  grur1a  8629  axgroth6  8638  mrcflem  13760  mrcval  13764  isacs2  13807  acsfiel  13808  ipoval  14509  fpwipodrs  14519  ipodrsima  14520  mreclat  14542  slwispgp  15174  pgpssslw  15177  lsmss1b  15228  lsmss2b  15230  lspf  15979  lspval  15980  lbsextlem1  16159  lbsextlem3  16161  lbsextlem4  16162  aspval  16316  mplsubglem  16427  mpllsslem  16428  basis2  16941  eltg2  16948  clsval  17026  clscld  17036  clsval2  17039  ntrcls0  17065  isnei  17092  neiint  17093  neips  17102  opnneissb  17103  opnssneib  17104  neindisj2  17112  innei  17114  neiptoptop  17120  neiptopnei  17121  neitr  17168  restcls  17169  cnpimaex  17244  cnprest2  17278  regsep  17322  nrmsep3  17343  nrmsep  17345  regsep2  17364  tgcmp  17388  uncmp  17390  1stcfb  17431  1stcrest  17439  2ndcctbss  17441  1stcelcls  17447  lly1stc  17482  xkoopn  17544  neitx  17562  txcnp  17575  txcmplem1  17596  kqnrmlem1  17698  kqnrmlem2  17699  nrmhmph  17749  fbssfi  17792  opnfbas  17797  fbasfip  17823  fbunfip  17824  fgss2  17829  fgcl  17833  supfil  17850  isufil2  17863  filssufilg  17866  ssufl  17873  ufileu  17874  elfm3  17905  fmfnfm  17913  ufldom  17917  fbflim2  17932  flfneii  17947  flftg  17951  txflf  17961  supnfcls  17975  fclscf  17980  fclsfnflim  17982  flimfnfcls  17983  alexsubALTlem2  18002  alexsubALTlem3  18003  alexsubALTlem4  18004  alexsubALT  18005  tsmsfbas  18080  tsmsres  18096  tsmsf1o  18097  tsmsxplem1  18105  tsmsxp  18107  ustssel  18158  ustincl  18160  ustdiag  18161  ustinvel  18162  ustexhalf  18163  ust0  18172  elutop  18186  ustuqtop4  18197  cfiluexsm  18243  cfiluweak  18248  blss  18348  metss  18430  metrest  18446  metcnp3  18462  metnrmlem3  18764  lebnumlem3  18861  lebnum  18862  ellimc3  19635  lhop1lem  19766  dchrelbas  20889  avril1  21607  resgrprn  21718  spanval  22685  spancl  22688  shsval2i  22739  omlsi  22756  ococin  22760  chsupsn  22765  pjoml  22788  shs00i  22802  chj00i  22839  chsscon3  22852  chlejb1  22864  chnle  22866  pjoml2  22963  pjoml3  22964  lecm  22969  stcltr1i  23627  mdbr  23647  dmdmd  23653  dmdi  23655  dmdbr3  23658  dmdbr4  23659  mdsl1i  23674  mdslmd1lem3  23680  mdslmd1lem4  23681  csmdsymi  23687  hatomic  23713  chrelat2  23723  atord  23741  atcvat4i  23750  sigagenval  24321  dmsigagen  24325  sigagenss  24330  kur14lem9  24681  dfrtrcl2  24929  fprodss  25055  wfrlem1  25282  wfrlem4  25285  wfrlem15  25296  frrlem1  25307  frrlem4  25310  frrlem5e  25315  frrlem11  25319  altopthsn  25522  bpolyval  25811  ssref  26056  refref  26058  fnessref  26066  refssfne  26067  comppfsc  26080  topjoin  26087  neifg  26093  totbndss  26179  heibor1lem  26211  unichnidl  26334  ispridl  26337  maxidlmax  26346  igenval  26364  igenidl  26366  igenmin  26367  igenval2  26369  nacsfix  26459  mzpcompact2  26502  rgspnval  27044  rgspncl  27045  rgspnmin  27047  ssrecnpr  27208  bnj1286  28728  bnj1452  28761  lsatcmp  29120  lcvexchlem4  29154  lcvexchlem5  29155  pclvalN  30006  pclclN  30007  elpcliN  30009  docaclN  31241  dihglb2  31459  doch2val2  31481  dochocss  31483  dochexmidlem7  31583  lpolconN  31604  mapdval  31745
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-in 3272  df-ss 3279
  Copyright terms: Public domain W3C validator