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

Theorem sseq2 3818
Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
Assertion
Ref Expression
sseq2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))

Proof of Theorem sseq2
StepHypRef Expression
1 sstr2 3799 . . . 4 (𝐶𝐴 → (𝐴𝐵𝐶𝐵))
21com12 32 . . 3 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
3 sstr2 3799 . . . 4 (𝐶𝐵 → (𝐵𝐴𝐶𝐴))
43com12 32 . . 3 (𝐵𝐴 → (𝐶𝐵𝐶𝐴))
52, 4anim12i 602 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
6 eqss 3807 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
7 dfbi2 462 . 2 ((𝐶𝐴𝐶𝐵) ↔ ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
85, 6, 73imtr4i 283 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wss 3763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-in 3770  df-ss 3777
This theorem is referenced by:  sseq12  3819  sseq2i  3821  sseq2d  3824  syl5sseq  3844  nssne1  3852  psseq2  3887  sseq0  4167  un00  4203  disjpss  4219  pweq  4348  ssintab  4679  ssintub  4680  intmin  4682  treq  4945  al0ssb  4979  sseliALT  4980  ssexg  4993  intabs  5011  iunopeqop  5170  ordunidif  5980  ordssun  6034  fununi  6169  feq3  6233  ssimaexg  6479  iunpw  7202  tfindsg  7284  limomss  7294  findsg  7317  funcnvuni  7343  frxp  7515  wrecseq123  7637  wfrlem1  7643  wfrlem4  7647  wfrlem4OLD  7648  wfrlem15  7659  onfununi  7668  oawordeu  7866  oawordexr  7867  nnawordex  7948  ereq1  7980  xpider  8047  domeng  8200  sbthlem4  8306  sbthlem5  8307  domssex  8354  finsschain  8506  dffi2  8562  dffi3  8570  hartogslem1  8680  inf3lema  8762  cantnflem1  8827  tz9.1  8846  tz9.1c  8847  tctr  8857  tcmin  8858  tcrank  8988  scottex  8989  cardlim  9075  infxpenlem  9113  infxpenc2  9122  isinfcard  9192  alephinit  9195  alephval3  9210  dfac3  9221  cflem  9347  cfval  9348  cflecard  9354  cfsuc  9358  cff1  9359  cfflb  9360  cflim2  9364  isf32lem2  9455  fin1a2lem13  9513  ac7g  9575  ttukeylem5  9614  ttukeylem7  9616  pwcfsdom  9684  pwfseqlem5  9764  pwfseq  9765  gch2  9776  winalim  9796  wunex  9840  wuncss  9846  eltskg  9851  eltsk2g  9852  gruina  9919  grur1a  9920  axgroth6  9929  swrdnd2  13651  trcleq2lem  13949  dfrtrcl2  14019  fprodss  14893  mrcflem  16465  mrcval  16469  isacs2  16512  acsfiel  16513  ipoval  17353  fpwipodrs  17363  ipodrsima  17364  mreclatBAD  17386  slwispgp  18221  pgpssslw  18224  lsmss1b  18275  lsmss2b  18277  cntzcmnss  18441  gsumzres  18505  lspf  19175  lspval  19176  lbsextlem1  19361  lbsextlem3  19363  lbsextlem4  19364  aspval  19531  mplsubglem  19637  mpllsslem  19638  basis2  20963  eltg2  20970  clsval  21049  clscld  21059  clsval2  21062  ntrcls0  21088  isnei  21115  neiint  21116  neips  21125  opnneissb  21126  opnssneib  21127  neindisj2  21135  innei  21137  neiptoptop  21143  neiptopnei  21144  neitr  21192  restcls  21193  cnpimaex  21268  cnprest2  21302  regsep  21346  nrmsep3  21367  nrmsep  21369  regsep2  21388  tgcmp  21412  uncmp  21414  bwth  21421  1stcfb  21456  1stcrest  21464  2ndcctbss  21466  1stcelcls  21472  lly1stc  21507  ssref  21523  refref  21524  comppfsc  21543  xkoopn  21600  neitx  21618  txcnp  21631  txcmplem1  21652  kqnrmlem1  21754  kqnrmlem2  21755  nrmhmph  21805  fbssfi  21848  opnfbas  21853  fbasfip  21879  fbunfip  21880  fgss2  21885  fgcl  21889  supfil  21906  isufil2  21919  filssufilg  21922  ssufl  21929  ufileu  21930  elfm3  21961  fmfnfm  21969  ufldom  21973  fbflim2  21988  flfneii  22003  flftg  22007  txflf  22017  supnfcls  22031  fclscf  22036  fclsfnflim  22038  flimfnfcls  22039  alexsubALTlem2  22059  alexsubALTlem3  22060  alexsubALTlem4  22061  alexsubALT  22062  tsmsfbas  22138  tsmsres  22154  tsmsf1o  22155  tsmsxplem1  22163  tsmsxp  22165  ustssel  22216  ustincl  22218  ustdiag  22219  ustinvel  22220  ustexhalf  22221  ust0  22230  elutop  22244  ustuqtop4  22255  cfiluexsm  22301  cfiluweak  22306  blssps  22436  blss  22437  metss  22520  metrest  22536  metcnp3  22552  metnrmlem3  22871  lebnumlem3  22969  lebnum  22970  ellimc3  23851  lhop1lem  23984  dchrelbas  25169  upgredgpr  26246  dfnbgr3  26441  nbupgr  26450  nbumgrvtx  26452  nbgr2vtx1edg  26456  nbuhgr2vtx1edgb  26458  cusgrexilem2  26560  wlkvtxiedg  26742  wlkres  26789  upgr1wlkdlem2  27313  1pthon2v  27320  1pthon2ve  27321  cusconngr  27358  avril1  27644  spanval  28514  spancl  28517  shsval2i  28568  omlsi  28585  ococin  28589  chsupsn  28594  pjoml  28617  shs00i  28631  chj00i  28668  chsscon3  28681  chlejb1  28693  chnle  28695  pjoml2  28792  pjoml3  28793  lecm  28798  stcltr1i  29455  mdbr  29475  dmdmd  29481  dmdi  29483  dmdbr3  29486  dmdbr4  29487  mdsl1i  29502  mdslmd1lem3  29508  mdslmd1lem4  29509  csmdsymi  29515  hatomic  29541  chrelat2  29551  atord  29569  atcvat4i  29578  fz1nntr  29882  reff  30225  cmpcref  30236  sigagenval  30522  dmsigagen  30526  sigagenss  30531  ldsysgenld  30542  ldgenpisyslem1  30545  ldgenpisyslem2  30546  dynkin  30549  carsgmon  30695  carsgclctunlem2  30700  bnj1286  31404  bnj1452  31437  kur14lem9  31513  mclsssvlem  31776  mclsind  31784  frrlem1  32095  scutun12  32232  imagesset  32375  altopthsn  32383  fnessref  32667  refssfne  32668  topjoin  32675  neifg  32681  bj-snglex  33265  relowlssretop  33521  relowlpssretop  33522  finxpreclem3  33540  poimirlem29  33745  poimir  33749  mblfinlem3  33755  totbndss  33881  heibor1lem  33913  unichnidl  34135  ispridl  34138  maxidlmax  34147  igenval  34165  igenidl  34167  igenmin  34168  igenval2  34170  brssr  34558  lsatcmp  34777  lcvexchlem4  34811  lcvexchlem5  34812  pclvalN  35664  pclclN  35665  elpcliN  35667  docaclN  36899  dihglb2  37117  doch2val2  37139  dochocss  37141  dochexmidlem7  37241  lpolconN  37262  mapdval  37403  nacsfix  37771  mzpcompact2  37811  rgspnval  38233  rgspncl  38234  rgspnmin  38236  superficl  38366  superuncl  38367  cleq2lem  38408  clcnvlem  38424  dfrtrcl3  38519  clsk1indlem2  38834  neik0pk1imk0  38839  isotone1  38840  isotone2  38841  ntrclsiso  38859  gneispacess2  38938  ssrecnpr  39001  founiiun  39843  founiiun0  39860  islptre  40325  salgenval  41014  salgenn0  41022  salgencl  41023  sssalgen  41026  salgenss  41027  salgenuni  41028  issalgend  41029  dfsalgen2  41032  salgencntex  41034  setrec1lem1  42996  setrec1lem3  42998  setrec2fun  43001
  Copyright terms: Public domain W3C validator