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

Theorem sseq2d 3666
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 3660 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  sseq12d  3667  sseqtrd  3674  sbcrel  5239  funimass2  6010  fnco  6037  fnssresb  6041  fnimaeq0  6051  foimacnv  6192  fvelimab  6292  ssimaexg  6303  knatar  6647  wfrdmcl  7468  wfrlem12  7471  onfununi  7483  oaordi  7671  oawordeulem  7679  oaass  7686  odi  7704  omass  7705  oen0  7711  oelim2  7720  nnaordi  7743  nnawordex  7762  pssnn  8219  fissuni  8312  dffi3  8378  cantnfle  8606  cantnflem1  8624  trcl  8642  r1sdom  8675  iscard2  8840  alephordi  8935  alephgeom  8943  cardaleph  8950  cardalephex  8951  ackbij2lem4  9102  cflm  9110  cfslbn  9127  cofsmo  9129  cfsmolem  9130  cfcoflem  9132  coftr  9133  alephsing  9136  fin23lem28  9200  fin23lem30  9202  fin23lem33  9205  fin1a2lem9  9268  axdc3lem2  9311  ttukeylem5  9373  fpwwe2lem5  9494  pwfseqlem4a  9521  pwfseqlem4  9522  wunex2  9598  inar1  9635  sstskm  9702  fsuppmapnn0fiubex  12832  swrdnd  13478  swrd0  13480  repswswrd  13577  rtrclreclem1  13842  rtrclreclem2  13843  summolem2  14491  summo  14492  zsum  14493  sumz  14497  sumss  14499  fsumcvg3  14504  prodmolem2  14709  prodmo  14710  zprod  14711  prod1  14718  vdwlem1  15732  vdwlem12  15743  vdwlem13  15744  ramub2  15765  rami  15766  ramz2  15775  setsstruct2  15943  prdsval  16162  pwsle  16199  mrcuni  16328  gsumpropd  17319  gsumpropd2lem  17320  gsumress  17323  eqgfval  17689  sscntz  17805  resscntz  17810  lsmlub  18124  efgrelexlemb  18209  efgcpbllemb  18214  gsumval3a  18350  gsumzaddlem  18367  gsumzoppg  18390  dmdprd  18443  dprdcntz  18453  subgdmdprd  18479  subrgpropd  18862  islss  18983  lsslss  19009  lsspropd  19065  lsmelpr  19139  lbspropd  19147  ltbval  19519  opsrval  19522  lsslinds  20218  isbasisg  20799  tgval  20807  tgss3  20838  restbas  21010  tgrest  21011  restcld  21024  restopn2  21029  restntr  21034  cnpnei  21116  cncls2  21125  perfcls  21217  cmpsublem  21250  cmpsub  21251  cmpcld  21253  uncmp  21254  hauscmplem  21257  cmpfi  21259  nconnsubb  21274  clsconn  21281  hausllycmp  21345  1stckgenlem  21404  txbas  21418  ptbasfi  21432  txcnpi  21459  ptcnp  21473  txcmplem1  21492  txcmplem2  21493  xkococnlem  21510  qtopcld  21564  fbasssin  21687  fbssint  21689  fbun  21691  fbasrn  21735  filufint  21771  ufinffr  21780  ufildr  21782  ustval  22053  trust  22080  elmopn  22294  neibl  22353  cfilucfil  22411  icccmplem1  22672  icccmplem2  22673  bndth  22804  isphtpc  22840  metcld  23150  bcthlem1  23167  bcth  23172  ovolfioo  23282  ovolficc  23283  elovolmr  23290  ovoliunlem3  23318  ovolicc2  23336  volsuplem  23369  dyadmax  23412  dyadmbllem  23413  dyadmbl  23414  incistruhgr  26019  edgssv2  26135  wksfval  26561  2wlkdlem9  26899  3wlkdlem9  27146  isfrgr  27238  sspval  27706  ubth  27857  orthin  28433  chssoc  28483  chsscon3  28487  chsscon1  28488  h1datom  28569  pjoml6i  28576  osum  28632  spansncv  28640  pjcjt2  28679  pjopyth  28707  hstel2  29206  hstle  29217  stj  29222  dmdbr5  29295  mdslmd1lem1  29312  atord  29375  chirredlem4  29380  atcvat4i  29384  mdsymlem2  29391  mdsymlem3  29392  mdsymlem8  29397  padct  29625  ssnnssfz  29677  tpr2rico  30086  ordtrestNEW  30095  sigaval  30301  issiga  30302  issgon  30314  oms0  30487  omssubadd  30490  kur14  31324  cvmliftlem15  31406  mclsrcl  31584  mclsval  31586  trpredtr  31854  dftrpred3g  31857  frecseq123  31902  frrlem4  31908  frrlem5e  31913  ivthALT  32455  isfne  32459  topfne  32474  neibastop3  32482  tailfb  32497  filnetlem1  32498  filnetlem4  32501  csbwrecsg  33303  relowlssretop  33341  poimirlem24  33563  mblfinlem2  33577  sstotbnd2  33703  sstotbnd  33704  sstotbnd3  33705  ssbnd  33717  cntotbnd  33725  cnpwstotbnd  33726  ismtyres  33737  heibor1lem  33738  heiborlem1  33740  heiborlem6  33745  heiborlem8  33747  exidreslem  33806  scottexf  34106  scott0f  34107  dfrefrels2  34403  dfrefrel2  34405  lshpcmp  34593  lsmsat  34613  lsmsatcv  34615  lfl1dim  34726  lfl1dim2N  34727  lkrss2N  34774  psubspset  35348  paddss  35449  psubclsetN  35540  dilfsetN  35757  dilsetN  35758  diaglbN  36661  dibglbN  36772  dihlspsnat  36939  dihglb2  36948  dochffval  36955  dochfval  36956  dochvalr  36963  dochord2N  36977  dochsncom  36988  dihjat1lem  37034  dvh4dimat  37044  dvh3dimatN  37045  dvh2dimatN  37046  dochexmidlem1  37066  lpolsetN  37088  lpolconN  37093  hdmaplkr  37522  hdmapoc  37540  hlhillcs  37567  ismrc  37581  incssnn0  37591  nacsfix  37592  hbt  38017  ss2iundf  38268  clsk1indlem1  38660  clsk1independent  38661  isotone1  38663  isotone2  38664  ntrclsiso  38682  ntrclsk2  38683  ssinc  39578  uzfissfz  39855  stoweidlem50  40585  stoweidlem57  40592  fourierdlem20  40662  fourierdlem50  40691  fourierdlem64  40705  fourierdlem86  40727  fourierdlem103  40744  fourierdlem104  40745  ovnval  41076  hoicvrrex  41091  ovnlecvr  41093  ovncvrrp  41099  ovnsubaddlem1  41105  hoidmvlelem3  41132  hoidmvle  41135  ovnhoilem1  41136  ovnhoi  41138  ovnlecvr2  41145  ovncvr2  41146  hspmbl  41164  ovolval4lem2  41185  ovolval5lem2  41188  ovolval5lem3  41189  ovolval5  41190  ovnovollem1  41191  ovnovollem2  41192  sprsymrelfvlem  42065  uspgrsprf  42079  uspgrsprfo  42081  ssnn0ssfz  42452  lincfsuppcl  42527
  Copyright terms: Public domain W3C validator