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

Theorem sseq2d 4003
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 3997 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  wss 3940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-in 3947  df-ss 3956
This theorem is referenced by:  sseq12d  4004  sseqtrd  4011  sbcrel  5654  funimass2  6434  fnco  6462  fnssresb  6466  fnimaeq0  6478  foimacnv  6629  fvelimab  6734  ssimaexg  6746  knatar  7102  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  17877  gsumpropd2lem  17878  gsumress  17881  eqgfval  18258  sscntz  18386  resscntz  18392  lsmlub  18710  efgrelexlemb  18796  efgcpbllemb  18801  gsumval3a  18943  gsumzaddlem  18961  gsumzoppg  18984  dmdprd  19040  dprdcntz  19050  subgdmdprd  19076  subrgpropd  19490  islss  19626  lsslss  19653  lsspropd  19709  lsmelpr  19783  lbspropd  19791  ltbval  20170  opsrval  20173  mhpval  20250  lsslinds  20891  isbasisg  21471  tgval  21479  tgss3  21510  restbas  21682  tgrest  21683  restcld  21696  restopn2  21701  restntr  21706  cnpnei  21788  cncls2  21797  perfcls  21889  cmpsublem  21923  cmpsub  21924  cmpcld  21926  uncmp  21927  hauscmplem  21930  cmpfi  21932  nconnsubb  21947  clsconn  21954  hausllycmp  22018  1stckgenlem  22077  txbas  22091  ptbasfi  22105  txcnpi  22132  ptcnp  22146  txcmplem1  22165  txcmplem2  22166  xkococnlem  22183  qtopcld  22237  fbasssin  22360  fbssint  22362  fbun  22364  fbasrn  22408  filufint  22444  ufinffr  22453  ufildr  22455  ustval  22726  trust  22753  elmopn  22967  neibl  23026  cfilucfil  23084  icccmplem1  23345  icccmplem2  23346  bndth  23477  isphtpc  23513  metcld  23824  bcthlem1  23842  bcth  23847  ovolfioo  23983  ovolficc  23984  elovolmr  23992  ovoliunlem3  24020  ovolicc2  24038  volsuplem  24071  dyadmax  24114  dyadmbllem  24115  dyadmbl  24116  incistruhgr  26778  edgssv2  26894  wksfval  27305  2wlkdlem9  27627  3wlkdlem9  27861  sspval  28414  ubth  28564  orthin  29137  chssoc  29187  chsscon3  29191  chsscon1  29192  h1datom  29273  pjoml6i  29280  osum  29336  spansncv  29344  pjcjt2  29383  pjopyth  29411  hstel2  29910  hstle  29921  stj  29926  dmdbr5  29999  mdslmd1lem1  30016  atord  30079  chirredlem4  30084  atcvat4i  30088  mdsymlem2  30095  mdsymlem3  30096  mdsymlem8  30101  padct  30368  ssnnssfz  30423  lindspropd  30857  tpr2rico  31041  ordtrestNEW  31050  sigaval  31256  issiga  31257  issgon  31268  oms0  31441  omssubadd  31444  subgrwlk  32263  umgr2cycllem  32271  kur14  32347  cvmliftlem15  32429  satfsschain  32495  mclsrcl  32692  mclsval  32694  trpredtr  32953  dftrpred3g  32956  frecseq123  33003  frrlem4  33010  ivthALT  33567  isfne  33571  topfne  33586  neibastop3  33594  tailfb  33609  filnetlem1  33610  filnetlem4  33613  csbwrecsg  34477  relowlssretop  34513  rdgssun  34528  poimirlem24  34783  mblfinlem2  34797  sstotbnd2  34920  sstotbnd  34921  sstotbnd3  34922  ssbnd  34934  cntotbnd  34942  cnpwstotbnd  34943  ismtyres  34954  heibor1lem  34955  heiborlem1  34957  heiborlem6  34962  heiborlem8  34964  exidreslem  35023  scottexf  35314  scott0f  35315  dfrefrels2  35620  dfrefrel2  35622  lshpcmp  35991  lsmsat  36011  lsmsatcv  36013  lfl1dim  36124  lfl1dim2N  36125  lkrss2N  36172  psubspset  36747  paddss  36848  psubclsetN  36939  dilfsetN  37155  dilsetN  37156  diaglbN  38058  dibglbN  38169  dihlspsnat  38336  dihglb2  38345  dochffval  38352  dochfval  38353  dochvalr  38360  dochord2N  38374  dochsncom  38385  dihjat1lem  38431  dvh4dimat  38441  dvh3dimatN  38442  dvh2dimatN  38443  dochexmidlem1  38463  lpolsetN  38485  lpolconN  38490  hdmaplkr  38916  hdmapoc  38934  hlhillcs  38961  ismrc  39163  incssnn0  39173  nacsfix  39174  hbt  39595  ss2iundf  39869  clsk1indlem1  40260  clsk1independent  40261  isotone1  40263  isotone2  40264  ntrclsiso  40282  ntrclsk2  40283  scottelrankd  40448  ssinc  41218  uzfissfz  41459  stoweidlem50  42201  stoweidlem57  42208  fourierdlem20  42278  fourierdlem50  42307  fourierdlem64  42321  fourierdlem86  42343  fourierdlem103  42360  fourierdlem104  42361  ovnval  42689  hoicvrrex  42704  ovnlecvr  42706  ovncvrrp  42712  ovnsubaddlem1  42718  hoidmvlelem3  42745  hoidmvle  42748  ovnhoilem1  42749  ovnhoi  42751  ovnlecvr2  42758  ovncvr2  42759  hspmbl  42777  ovolval4lem2  42798  ovolval5lem2  42801  ovolval5lem3  42802  ovolval5  42803  ovnovollem1  42804  ovnovollem2  42805  sprsymrelfvlem  43484  uspgrsprf  43853  uspgrsprfo  43855  ssnn0ssfz  44229  lincfsuppcl  44300
  Copyright terms: Public domain W3C validator