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

Theorem sseq1d 3335
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 3329 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    C_ wss 3280
This theorem is referenced by:  sseq12d  3337  eqsstrd  3342  snssg  3892  ssiun2s  4095  disjxiun  4169  treq  4268  funimass1  5485  feq1  5535  fvmptss  5772  fvimacnvi  5803  fvimacnvALT  5808  fnsuppres  5911  knatar  6039  ovmptss  6387  oaordi  6748  oaword2  6755  oawordeulem  6756  omword1  6775  oewordri  6794  oeordsuc  6796  nnaordi  6820  nnawordex  6839  ereq1  6871  elpm2r  6993  inficl  7388  fipwss  7392  dffi3  7394  hartogslem1  7467  inf3lema  7535  inf3lemd  7538  cantnfle  7582  cantnflem2  7602  trcl  7620  tcmin  7636  rankr1ai  7680  rankxplim  7759  scottex  7765  scott0  7766  scottexs  7767  scott0s  7768  karden  7775  cardne  7808  cardaleph  7926  ackbij2  8079  cflim2  8099  cfslb  8102  coftr  8109  fin23lem15  8170  fin23lem32  8180  fin23lem34  8182  fin23lem35  8183  fin23lem36  8184  fin23lem41  8188  isf32lem1  8189  itunitc1  8256  axdc3lem2  8287  ttukeylem1  8345  fpwwe2cbv  8461  fpwwe2lem2  8463  fpwwe2  8474  fpwwecbv  8475  fpwwelem  8476  canthwelem  8481  canthwe  8482  wunex2  8569  wuncval2  8578  eltsk2g  8582  tskpwss  8583  inar1  8606  grothpw  8657  grothpwex  8658  axgroth6  8659  grothac  8661  peano5uzti  10315  lo1o1  12281  o1lo1  12286  o1lo12  12287  lo1eq  12317  rlimeq  12318  isercoll  12416  prmreclem4  13242  vdwmc  13301  vdwlem1  13304  vdwlem2  13305  vdwlem12  13315  vdwlem13  13316  ramval  13331  ramz2  13347  ramub1lem1  13349  isacs2  13833  isacs1i  13837  mreacs  13838  acsfn  13839  rescabs  13988  ipole  14539  ipodrsima  14546  isacs5  14553  sylow1  15192  efgval2  15311  efgsfo  15326  frgpuplem  15359  dprdcntz  15521  islbs2  16181  pptbas  17027  pnfnei  17238  mnfnei  17239  iscnp  17255  iscnp4  17281  cnntr  17293  cnconst2  17301  cnpresti  17306  cnprest  17307  isreg  17350  isnrm  17353  isnrm2  17376  perfcls  17383  isreg2  17395  hauscmplem  17423  1stcfb  17461  1stcelcls  17477  1stccnp  17478  txbas  17552  ptbasfi  17566  xkoopn  17574  xkoccn  17604  txcnp  17605  ptcnplem  17606  txdis  17617  txdis1cn  17620  txtube  17625  txkgen  17637  xkohaus  17638  xkoptsub  17639  xkoco1cn  17642  xkoco2cn  17643  xkococnlem  17644  xkococn  17645  xkoinjcn  17672  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  reghmph  17778  nrmhmph  17779  trfil2  17872  ufileu  17904  elfm  17932  elfm2  17933  elfm3  17935  imaelfm  17936  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  fmco  17946  elflim2  17949  flffbas  17980  lmflf  17990  txflf  17991  fclscf  18010  flimfnfcls  18013  cnextcn  18051  symgtgp  18084  ghmcnp  18097  divstgplem  18103  eltsms  18115  ustval  18185  ust0  18202  trust  18212  utoptop  18217  restutop  18220  restutopopn  18221  utopsnneiplem  18230  ucncn  18268  fmucnd  18275  cfilufg  18276  trcfilu  18277  neipcfilu  18279  blssps  18407  blss  18408  ssblex  18411  blin2  18412  metss2  18495  metrest  18507  metcnp3  18523  metustexhalfOLD  18546  metustexhalf  18547  metustblOLD  18563  metustbl  18564  metutopOLD  18565  psmetutop  18566  xrsmopn  18796  recld2  18798  icccmplem1  18806  icccmplem2  18807  icccmp  18809  reconnlem2  18811  lebnumlem3  18941  lebnum  18942  xlebnum  18943  lebnumii  18944  nmhmcn  19081  cfilfval  19170  caubl  19213  caublcls  19214  bcthlem1  19230  bcth  19235  ovolfiniun  19350  ovoliunlem3  19353  ovoliun  19354  ovoliun2  19355  ovoliunnul  19356  voliunlem3  19399  dyadmax  19443  dyadmbllem  19444  dyadmbl  19445  opnmbllem  19446  ellimc2  19717  limcnlp  19718  ellimc3  19719  limcflf  19721  limciun  19734  cpnord  19774  lhop  19853  xrlimcnp  20760  cvxcl  20776  dchrval  20971  isssp  22176  ubthlem1  22325  shmodi  22845  chsupid  22867  chsscon3  22955  spansncvi  23107  mdslmd1lem3  23783  mdslmd1lem4  23784  mdsymlem5  23863  dmdbr5ati  23878  dmdbr6ati  23879  dmdbr7ati  23880  ssiun2sf  23963  tpr2rico  24263  pnfneige0  24289  rrhre  24340  dya2icoseg2  24581  kur14  24855  cvmliftlem15  24938  cvmlift2lem12  24954  cvmlift2lem13  24955  relexpdm  25088  relexprn  25089  rtrclreclem.min  25100  dfrtrcl2  25101  dfpo2  25326  preddowncl  25410  trpredlem1  25444  trpredmintr  25448  wfrlem1  25470  wfrlem3  25472  wfrlem9  25478  wfrlem15  25484  tfrALTlem  25490  frrlem1  25495  frrlem4  25498  frrlem5e  25503  nobndup  25568  nobnddown  25569  nofulllem5  25574  bpolyval  25999  mblfinlem  26143  mblfinlem2  26144  ovoliunnfl  26147  ex-ovoliunnfl  26148  voliunnfl  26149  opnrebl  26213  opnrebl2  26214  ivthALT  26228  neibastop2lem  26279  fnemeet1  26285  filnetlem1  26297  filnetlem4  26300  totbndbnd  26388  heibor1lem  26408  heiborlem10  26419  ismrcd1  26642  nacsfix  26656  setindtr  26985  frlmssuvc1  27114  frlmssuvc2  27115  frlmsslsp  27116  hbtlem6  27201  symgsssg  27276  psgnunilem5  27285  frgraunss  28099  frgra1v  28102  frgra2v  28103  frgra3vlem1  28104  frgra3vlem2  28105  frgra3v  28106  4cycl2vnunb  28121  n4cyclfrgra  28122  bnj517  28962  bnj1014  29037  bnj1015  29038  bnj1123  29061  bnj1125  29067  bnj1450  29125  bnj1452  29127  lcv1  29524  lfl1dim  29604  lfl1dim2N  29605  paddasslem17  30318  dihglblem6  31823  dochvalr  31840  dochord3  31855  lpolconN  31970  lcfls1lem  32017  mapdffval  32109  mapdfval  32110  mapdsn2  32125  mapd0  32148  lspindp5  32253  mapdh8ab  32260
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator