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

Theorem sseq2d 3998
Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
sseq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
sseq2d (𝜑 → (𝐶𝐴𝐶𝐵))

Proof of Theorem sseq2d
StepHypRef Expression
1 sseq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 sseq2 3992 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  sseq12d  3999  sseqtrd  4006  sbcrel  5649  funimass2  6431  fnco  6459  fnssresb  6463  fnimaeq0  6475  foimacnv  6626  fvelimab  6731  ssimaexg  6743  knatar  7099  wfrdmcl  7954  wfrlem12  7957  onfununi  7969  oaordi  8162  oawordeulem  8170  oaass  8177  odi  8195  omass  8196  oen0  8202  oelim2  8211  nnaordi  8234  nnawordex  8253  pssnn  8725  fissuni  8818  dffi3  8884  cantnfle  9123  cantnflem1  9141  trcl  9159  r1sdom  9192  iscard2  9394  alephordi  9489  alephgeom  9497  cardaleph  9504  cardalephex  9505  ackbij2lem4  9653  cflm  9661  cfslbn  9678  cofsmo  9680  cfsmolem  9681  cfcoflem  9683  coftr  9684  alephsing  9687  fin23lem28  9751  fin23lem30  9753  fin23lem33  9756  fin1a2lem9  9819  axdc3lem2  9862  ttukeylem5  9924  fpwwe2lem5  10045  pwfseqlem4a  10072  pwfseqlem4  10073  wunex2  10149  inar1  10186  sstskm  10253  fsuppmapnn0fiubex  13350  swrdnd  14006  swrd0  14010  repswswrd  14136  rtrclreclem1  14407  rtrclreclem2  14408  summolem2  15063  summo  15064  zsum  15065  sumz  15069  sumss  15071  fsumcvg3  15076  prodmolem2  15279  prodmo  15280  zprod  15281  prod1  15288  vdwlem1  16307  vdwlem12  16318  vdwlem13  16319  ramub2  16340  rami  16341  ramz2  16350  setsstruct2  16511  prdsval  16718  pwsle  16755  mrcuni  16882  gsumpropd  17878  gsumpropd2lem  17879  gsumress  17882  eqgfval  18268  sscntz  18396  resscntz  18402  lsmlub  18721  efgrelexlemb  18807  efgcpbllemb  18812  gsumval3a  18954  gsumzaddlem  18972  gsumzoppg  18995  dmdprd  19051  dprdcntz  19061  subgdmdprd  19087  subrgpropd  19501  islss  19637  lsslss  19664  lsspropd  19720  lsmelpr  19794  lbspropd  19802  ltbval  20182  opsrval  20185  mhpval  20263  lsslinds  20905  isbasisg  21485  tgval  21493  tgss3  21524  restbas  21696  tgrest  21697  restcld  21710  restopn2  21715  restntr  21720  cnpnei  21802  cncls2  21811  perfcls  21903  cmpsublem  21937  cmpsub  21938  cmpcld  21940  uncmp  21941  hauscmplem  21944  cmpfi  21946  nconnsubb  21961  clsconn  21968  hausllycmp  22032  1stckgenlem  22091  txbas  22105  ptbasfi  22119  txcnpi  22146  ptcnp  22160  txcmplem1  22179  txcmplem2  22180  xkococnlem  22197  qtopcld  22251  fbasssin  22374  fbssint  22376  fbun  22378  fbasrn  22422  filufint  22458  ufinffr  22467  ufildr  22469  ustval  22740  trust  22767  elmopn  22981  neibl  23040  cfilucfil  23098  icccmplem1  23359  icccmplem2  23360  bndth  23491  isphtpc  23527  metcld  23838  bcthlem1  23856  bcth  23861  ovolfioo  23997  ovolficc  23998  elovolmr  24006  ovoliunlem3  24034  ovolicc2  24052  volsuplem  24085  dyadmax  24128  dyadmbllem  24129  dyadmbl  24130  incistruhgr  26792  edgssv2  26908  wksfval  27319  2wlkdlem9  27641  3wlkdlem9  27875  sspval  28428  ubth  28578  orthin  29151  chssoc  29201  chsscon3  29205  chsscon1  29206  h1datom  29287  pjoml6i  29294  osum  29350  spansncv  29358  pjcjt2  29397  pjopyth  29425  hstel2  29924  hstle  29935  stj  29940  dmdbr5  30013  mdslmd1lem1  30030  atord  30093  chirredlem4  30098  atcvat4i  30102  mdsymlem2  30109  mdsymlem3  30110  mdsymlem8  30115  padct  30382  ssnnssfz  30437  lindspropd  30871  tpr2rico  31055  ordtrestNEW  31064  sigaval  31270  issiga  31271  issgon  31282  oms0  31455  omssubadd  31458  subgrwlk  32277  umgr2cycllem  32285  kur14  32361  cvmliftlem15  32443  satfsschain  32509  mclsrcl  32706  mclsval  32708  trpredtr  32967  dftrpred3g  32970  frecseq123  33017  frrlem4  33024  ivthALT  33581  isfne  33585  topfne  33600  neibastop3  33608  tailfb  33623  filnetlem1  33624  filnetlem4  33627  csbwrecsg  34491  relowlssretop  34527  rdgssun  34542  poimirlem24  34798  mblfinlem2  34812  sstotbnd2  34935  sstotbnd  34936  sstotbnd3  34937  ssbnd  34949  cntotbnd  34957  cnpwstotbnd  34958  ismtyres  34969  heibor1lem  34970  heiborlem1  34972  heiborlem6  34977  heiborlem8  34979  exidreslem  35038  scottexf  35329  scott0f  35330  dfrefrels2  35635  dfrefrel2  35637  lshpcmp  36006  lsmsat  36026  lsmsatcv  36028  lfl1dim  36139  lfl1dim2N  36140  lkrss2N  36187  psubspset  36762  paddss  36863  psubclsetN  36954  dilfsetN  37170  dilsetN  37171  diaglbN  38073  dibglbN  38184  dihlspsnat  38351  dihglb2  38360  dochffval  38367  dochfval  38368  dochvalr  38375  dochord2N  38389  dochsncom  38400  dihjat1lem  38446  dvh4dimat  38456  dvh3dimatN  38457  dvh2dimatN  38458  dochexmidlem1  38478  lpolsetN  38500  lpolconN  38505  hdmaplkr  38931  hdmapoc  38949  hlhillcs  38976  ismrc  39178  incssnn0  39188  nacsfix  39189  hbt  39610  ss2iundf  39884  clsk1indlem1  40275  clsk1independent  40276  isotone1  40278  isotone2  40279  ntrclsiso  40297  ntrclsk2  40298  scottelrankd  40463  ssinc  41233  uzfissfz  41474  stoweidlem50  42216  stoweidlem57  42223  fourierdlem20  42293  fourierdlem50  42322  fourierdlem64  42336  fourierdlem86  42358  fourierdlem103  42375  fourierdlem104  42376  ovnval  42704  hoicvrrex  42719  ovnlecvr  42721  ovncvrrp  42727  ovnsubaddlem1  42733  hoidmvlelem3  42760  hoidmvle  42763  ovnhoilem1  42764  ovnhoi  42766  ovnlecvr2  42773  ovncvr2  42774  hspmbl  42792  ovolval4lem2  42813  ovolval5lem2  42816  ovolval5lem3  42817  ovolval5  42818  ovnovollem1  42819  ovnovollem2  42820  sprsymrelfvlem  43499  uspgrsprf  43868  uspgrsprfo  43870  ssnn0ssfz  44295  lincfsuppcl  44366
  Copyright terms: Public domain W3C validator