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

Theorem sseq1d 3371
Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
sseq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
sseq1d  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )

Proof of Theorem sseq1d
StepHypRef Expression
1 sseq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 sseq1 3365 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  sseq12d  3373  eqsstrd  3378  snssg  3995  ssiun2s  4202  disjxiun  4277  treq  4379  funimass1  5479  feq1  5530  fvmptss  5770  fvimacnvi  5805  fvimacnvALT  5810  fnsuppresOLD  5925  knatar  6035  ovmptss  6643  fnsuppres  6705  imacosupp  6718  oaordi  6973  oaword2  6980  oawordeulem  6981  omword1  7000  oewordri  7019  oeordsuc  7021  nnaordi  7045  nnawordex  7064  ereq1  7096  elpm2r  7218  inficl  7663  fipwss  7667  dffi3  7669  hartogslem1  7744  inf3lema  7818  inf3lemd  7821  cantnfle  7867  cantnflem2  7886  cantnfleOLD  7897  trcl  7936  tcmin  7949  rankr1ai  7993  rankxplim  8074  scottex  8080  scott0  8081  scottexs  8082  scott0s  8083  karden  8090  cardne  8123  cardaleph  8247  ackbij2  8400  cflim2  8420  cfslb  8423  coftr  8430  fin23lem15  8491  fin23lem32  8501  fin23lem34  8503  fin23lem35  8504  fin23lem36  8505  fin23lem41  8509  isf32lem1  8510  itunitc1  8577  axdc3lem2  8608  ttukeylem1  8666  fpwwe2cbv  8785  fpwwe2lem2  8787  fpwwe2  8798  fpwwecbv  8799  fpwwelem  8800  canthwelem  8805  canthwe  8806  wunex2  8893  wuncval2  8902  eltsk2g  8906  tskpwss  8907  inar1  8930  grothpw  8981  grothpwex  8982  axgroth6  8983  grothac  8985  peano5uzti  10719  lo1o1  12994  o1lo1  12999  o1lo12  13000  lo1eq  13030  rlimeq  13031  isercoll  13129  prmreclem4  13963  vdwmc  14022  vdwlem1  14025  vdwlem2  14026  vdwlem12  14036  vdwlem13  14037  ramval  14052  ramz2  14068  ramub1lem1  14070  isacs2  14574  isacs1i  14578  mreacs  14579  acsfn  14580  rescabs  14729  ipole  15311  ipodrsima  15318  isacs5  15325  symgsssg  15953  psgnunilem5  15980  sylow1  16082  efgval2  16201  efgsfo  16216  frgpuplem  16249  gsumzf1o  16371  gsumzmhm  16407  gsumzoppg  16416  dprdcntz  16466  islbs2  17157  frlmssuvc1  18061  frlmssuvc2  18062  frlmssuvc1OLD  18063  frlmssuvc2OLD  18064  frlmsslsp  18065  frlmsslspOLD  18066  pptbas  18454  pnfnei  18666  mnfnei  18667  iscnp  18683  iscnp4  18709  cnntr  18721  cnconst2  18729  cnpresti  18734  cnprest  18735  isreg  18778  isnrm  18781  isnrm2  18804  perfcls  18811  isreg2  18823  hauscmplem  18851  1stcfb  18891  1stcelcls  18907  1stccnp  18908  txbas  18982  ptbasfi  18996  xkoopn  19004  xkoccn  19034  txcnp  19035  ptcnplem  19036  txdis  19047  txdis1cn  19050  txtube  19055  txkgen  19067  xkohaus  19068  xkoptsub  19069  xkoco1cn  19072  xkoco2cn  19073  xkococnlem  19074  xkococn  19075  xkoinjcn  19102  kqreglem1  19156  kqreglem2  19157  kqnrmlem1  19158  kqnrmlem2  19159  reghmph  19208  nrmhmph  19209  trfil2  19302  ufileu  19334  elfm  19362  elfm2  19363  elfm3  19365  imaelfm  19366  rnelfm  19368  fmfnfmlem2  19370  fmfnfmlem4  19372  fmco  19376  elflim2  19379  flffbas  19410  lmflf  19420  txflf  19421  fclscf  19440  flimfnfcls  19443  cnextcn  19481  symgtgp  19514  ghmcnp  19527  divstgplem  19533  eltsms  19545  ustval  19619  ust0  19636  trust  19646  utoptop  19651  restutop  19654  restutopopn  19655  utopsnneiplem  19664  ucncn  19702  fmucnd  19709  cfilufg  19710  trcfilu  19711  neipcfilu  19713  blssps  19841  blss  19842  ssblex  19845  blin2  19846  metss2  19929  metrest  19941  metcnp3  19957  metustexhalfOLD  19980  metustexhalf  19981  metustblOLD  19997  metustbl  19998  metutopOLD  19999  psmetutop  20000  xrsmopn  20231  recld2  20233  icccmplem1  20241  icccmplem2  20242  icccmp  20244  reconnlem2  20246  lebnumlem3  20377  lebnum  20378  xlebnum  20379  lebnumii  20380  nmhmcn  20517  cfilfval  20617  caubl  20660  caublcls  20661  bcthlem1  20677  bcth  20682  ovolfiniun  20826  ovoliunlem3  20829  ovoliun  20830  ovoliun2  20831  ovoliunnul  20832  voliunlem3  20875  dyadmax  20920  dyadmbllem  20921  dyadmbl  20922  opnmbllem  20923  ellimc2  21194  limcnlp  21195  ellimc3  21196  limcflf  21198  limciun  21211  cpnord  21251  lhop  21330  xrlimcnp  22247  cvxcl  22263  dchrval  22458  isssp  23945  ubthlem1  24094  shmodi  24616  chsupid  24638  chsscon3  24726  spansncvi  24878  mdslmd1lem3  25554  mdslmd1lem4  25555  mdsymlem5  25634  dmdbr5ati  25649  dmdbr6ati  25650  dmdbr7ati  25651  ssiun2sf  25734  fpwrelmapffslem  25857  tpr2rico  26196  pnfneige0  26235  rrhre  26301  dya2icoseg2  26547  eulerpartlemt0  26600  eulerpartgbij  26603  eulerpartlemr  26605  eulerpartlemgs2  26611  eulerpartlemn  26612  eulerpart  26613  kur14  26952  cvmliftlem15  27035  cvmlift2lem12  27051  cvmlift2lem13  27052  relexpdm  27184  relexprn  27185  rtrclreclem.min  27196  dfrtrcl2  27197  dfpo2  27412  preddowncl  27504  trpredlem1  27538  trpredmintr  27542  wrecseq123  27565  wfrlem1  27571  wfrlem3  27573  wfrlem9  27579  wfrlem15  27585  frrlem1  27615  frrlem4  27618  frrlem5e  27623  nobndup  27688  nobnddown  27689  nofulllem5  27694  opnmbllem0  28271  mblfinlem1  28272  mblfinlem2  28273  mblfinlem3  28274  ovoliunnfl  28277  ex-ovoliunnfl  28278  voliunnfl  28279  opnrebl  28359  opnrebl2  28360  ivthALT  28374  neibastop2lem  28425  fnemeet1  28431  filnetlem1  28443  filnetlem4  28446  totbndbnd  28532  heibor1lem  28552  heiborlem10  28563  scottexf  28825  scott0f  28826  ismrcd1  28879  nacsfix  28893  setindtr  29218  hbtlem6  29330  frgraunss  30433  frgra1v  30436  frgra2v  30437  frgra3vlem1  30438  frgra3vlem2  30439  frgra3v  30440  4cycl2vnunb  30455  n4cyclfrgra  30456  bnj517  31580  bnj1014  31655  bnj1015  31656  bnj1123  31679  bnj1125  31685  bnj1450  31743  bnj1452  31745  lcv1  32259  lfl1dim  32339  lfl1dim2N  32340  paddasslem17  33053  dihglblem6  34558  dochvalr  34575  dochord3  34590  lpolconN  34705  lcfls1lem  34752  mapdffval  34844  mapdfval  34845  mapdsn2  34860  mapd0  34883  lspindp5  34988  mapdh8ab  34995
  Copyright terms: Public domain W3C validator