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

Theorem sseq2 3362
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 3347 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 29 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3347 . . . 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 3355 . 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 1652    C_ wss 3312
This theorem is referenced by:  sseq12  3363  sseq2i  3365  sseq2d  3368  syl5sseq  3388  nssne1  3396  psseq2  3427  sseq0  3651  un00  3655  disjpss  3670  pweq  3794  ssintab  4059  ssintub  4060  intmin  4062  treq  4300  ssexg  4341  intabs  4353  ordunidif  4621  ordssun  4672  iunpw  4750  tfindsg  4831  limomss  4841  findsg  4863  fununi  5508  funcnvuni  5509  feq3  5569  ssimaexg  5780  frxp  6447  onfununi  6594  oawordeu  6789  oawordexr  6790  nnawordex  6871  ereq1  6903  xpider  6966  domeng  7113  sbthlem4  7211  sbthlem5  7212  domssex  7259  finsschain  7404  dffi2  7419  dffi3  7427  hartogslem1  7500  inf3lema  7568  cantnflem1  7634  tz9.1  7654  tz9.1c  7655  tctr  7668  tcmin  7669  tcrank  7797  scottex  7798  cardlim  7848  infxpenlem  7884  infxpenc2  7892  isinfcard  7962  alephinit  7965  alephval3  7980  dfac3  7991  cflem  8115  cfval  8116  cflecard  8122  cfsuc  8126  cff1  8127  cfflb  8128  cflim2  8132  isf32lem2  8223  fin1a2lem13  8281  ac7g  8343  ttukeylem5  8382  ttukeylem7  8384  pwcfsdom  8447  pwfseqlem5  8527  pwfseq  8528  gch2  8543  winalim  8559  wunex  8603  wuncss  8609  eltskg  8614  eltsk2g  8615  gruina  8682  grur1a  8683  axgroth6  8692  mrcflem  13819  mrcval  13823  isacs2  13866  acsfiel  13867  ipoval  14568  fpwipodrs  14578  ipodrsima  14579  mreclat  14601  slwispgp  15233  pgpssslw  15236  lsmss1b  15287  lsmss2b  15289  lspf  16038  lspval  16039  lbsextlem1  16218  lbsextlem3  16220  lbsextlem4  16221  aspval  16375  mplsubglem  16486  mpllsslem  16487  basis2  17004  eltg2  17011  clsval  17089  clscld  17099  clsval2  17102  ntrcls0  17128  isnei  17155  neiint  17156  neips  17165  opnneissb  17166  opnssneib  17167  neindisj2  17175  innei  17177  neiptoptop  17183  neiptopnei  17184  neitr  17232  restcls  17233  cnpimaex  17308  cnprest2  17342  regsep  17386  nrmsep3  17407  nrmsep  17409  regsep2  17428  tgcmp  17452  uncmp  17454  bwth  17461  1stcfb  17496  1stcrest  17504  2ndcctbss  17506  1stcelcls  17512  lly1stc  17547  xkoopn  17609  neitx  17627  txcnp  17640  txcmplem1  17661  kqnrmlem1  17763  kqnrmlem2  17764  nrmhmph  17814  fbssfi  17857  opnfbas  17862  fbasfip  17888  fbunfip  17889  fgss2  17894  fgcl  17898  supfil  17915  isufil2  17928  filssufilg  17931  ssufl  17938  ufileu  17939  elfm3  17970  fmfnfm  17978  ufldom  17982  fbflim2  17997  flfneii  18012  flftg  18016  txflf  18026  supnfcls  18040  fclscf  18045  fclsfnflim  18047  flimfnfcls  18048  alexsubALTlem2  18067  alexsubALTlem3  18068  alexsubALTlem4  18069  alexsubALT  18070  tsmsfbas  18145  tsmsres  18161  tsmsf1o  18162  tsmsxplem1  18170  tsmsxp  18172  ustssel  18223  ustincl  18225  ustdiag  18226  ustinvel  18227  ustexhalf  18228  ust0  18237  elutop  18251  ustuqtop4  18262  cfiluexsm  18308  cfiluweak  18313  blssps  18442  blss  18443  metss  18526  metrest  18542  metcnp3  18558  metnrmlem3  18879  lebnumlem3  18976  lebnum  18977  ellimc3  19754  lhop1lem  19885  dchrelbas  21008  avril1  21745  resgrprn  21856  spanval  22823  spancl  22826  shsval2i  22877  omlsi  22894  ococin  22898  chsupsn  22903  pjoml  22926  shs00i  22940  chj00i  22977  chsscon3  22990  chlejb1  23002  chnle  23004  pjoml2  23101  pjoml3  23102  lecm  23107  stcltr1i  23765  mdbr  23785  dmdmd  23791  dmdi  23793  dmdbr3  23796  dmdbr4  23797  mdsl1i  23812  mdslmd1lem3  23818  mdslmd1lem4  23819  csmdsymi  23825  hatomic  23851  chrelat2  23861  atord  23879  atcvat4i  23888  sigagenval  24511  dmsigagen  24515  sigagenss  24520  kur14lem9  24888  dfrtrcl2  25136  fprodss  25263  wfrlem1  25511  wfrlem4  25514  wfrlem15  25525  frrlem1  25536  frrlem4  25539  frrlem5e  25544  frrlem11  25548  imagesset  25748  altopthsn  25754  bpolyval  26043  mblfinlem2  26191  ssref  26300  refref  26302  fnessref  26310  refssfne  26311  comppfsc  26324  topjoin  26331  neifg  26337  totbndss  26423  heibor1lem  26455  unichnidl  26578  ispridl  26581  maxidlmax  26590  igenval  26608  igenidl  26610  igenmin  26611  igenval2  26613  nacsfix  26703  mzpcompact2  26746  rgspnval  27288  rgspncl  27289  rgspnmin  27291  ssrecnpr  27452  bnj1286  29242  bnj1452  29275  lsatcmp  29640  lcvexchlem4  29674  lcvexchlem5  29675  pclvalN  30526  pclclN  30527  elpcliN  30529  docaclN  31761  dihglb2  31979  doch2val2  32001  dochocss  32003  dochexmidlem7  32103  lpolconN  32124  mapdval  32265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator