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

Theorem sseq1d 3378
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 3372 . 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 1369    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  sseq12d  3380  eqsstrd  3385  snssg  4002  ssiun2s  4209  disjxiun  4284  treq  4386  funimass1  5486  feq1  5537  fvmptss  5777  fvimacnvi  5812  fvimacnvALT  5817  fnsuppresOLD  5933  knatar  6043  ovmptss  6649  fnsuppres  6711  imacosupp  6724  oaordi  6977  oaword2  6984  oawordeulem  6985  omword1  7004  oewordri  7023  oeordsuc  7025  nnaordi  7049  nnawordex  7068  ereq1  7100  elpm2r  7222  inficl  7667  fipwss  7671  dffi3  7673  hartogslem1  7748  inf3lema  7822  inf3lemd  7825  cantnfle  7871  cantnflem2  7890  cantnfleOLD  7901  trcl  7940  tcmin  7953  rankr1ai  7997  rankxplim  8078  scottex  8084  scott0  8085  scottexs  8086  scott0s  8087  karden  8094  cardne  8127  cardaleph  8251  ackbij2  8404  cflim2  8424  cfslb  8427  coftr  8434  fin23lem15  8495  fin23lem32  8505  fin23lem34  8507  fin23lem35  8508  fin23lem36  8509  fin23lem41  8513  isf32lem1  8514  itunitc1  8581  axdc3lem2  8612  ttukeylem1  8670  fpwwe2cbv  8789  fpwwe2lem2  8791  fpwwe2  8802  fpwwecbv  8803  fpwwelem  8804  canthwelem  8809  canthwe  8810  wunex2  8897  wuncval2  8906  eltsk2g  8910  tskpwss  8911  inar1  8934  grothpw  8985  grothpwex  8986  axgroth6  8987  grothac  8989  peano5uzti  10723  lo1o1  13002  o1lo1  13007  o1lo12  13008  lo1eq  13038  rlimeq  13039  isercoll  13137  prmreclem4  13972  vdwmc  14031  vdwlem1  14034  vdwlem2  14035  vdwlem12  14045  vdwlem13  14046  ramval  14061  ramz2  14077  ramub1lem1  14079  isacs2  14583  isacs1i  14587  mreacs  14588  acsfn  14589  rescabs  14738  ipole  15320  ipodrsima  15327  isacs5  15334  symgsssg  15964  psgnunilem5  15991  sylow1  16093  efgval2  16212  efgsfo  16227  frgpuplem  16260  gsumzf1o  16382  gsumzmhm  16420  gsumzoppg  16430  dprdcntz  16482  islbs2  17215  frlmssuvc1  18199  frlmssuvc2  18200  frlmssuvc1OLD  18201  frlmssuvc2OLD  18202  frlmsslsp  18203  frlmsslspOLD  18204  pptbas  18592  pnfnei  18804  mnfnei  18805  iscnp  18821  iscnp4  18847  cnntr  18859  cnconst2  18867  cnpresti  18872  cnprest  18873  isreg  18916  isnrm  18919  isnrm2  18942  perfcls  18949  isreg2  18961  hauscmplem  18989  1stcfb  19029  1stcelcls  19045  1stccnp  19046  txbas  19120  ptbasfi  19134  xkoopn  19142  xkoccn  19172  txcnp  19173  ptcnplem  19174  txdis  19185  txdis1cn  19188  txtube  19193  txkgen  19205  xkohaus  19206  xkoptsub  19207  xkoco1cn  19210  xkoco2cn  19211  xkococnlem  19212  xkococn  19213  xkoinjcn  19240  kqreglem1  19294  kqreglem2  19295  kqnrmlem1  19296  kqnrmlem2  19297  reghmph  19346  nrmhmph  19347  trfil2  19440  ufileu  19472  elfm  19500  elfm2  19501  elfm3  19503  imaelfm  19504  rnelfm  19506  fmfnfmlem2  19508  fmfnfmlem4  19510  fmco  19514  elflim2  19517  flffbas  19548  lmflf  19558  txflf  19559  fclscf  19578  flimfnfcls  19581  cnextcn  19619  symgtgp  19652  ghmcnp  19665  divstgplem  19671  eltsms  19683  ustval  19757  ust0  19774  trust  19784  utoptop  19789  restutop  19792  restutopopn  19793  utopsnneiplem  19802  ucncn  19840  fmucnd  19847  cfilufg  19848  trcfilu  19849  neipcfilu  19851  blssps  19979  blss  19980  ssblex  19983  blin2  19984  metss2  20067  metrest  20079  metcnp3  20095  metustexhalfOLD  20118  metustexhalf  20119  metustblOLD  20135  metustbl  20136  metutopOLD  20137  psmetutop  20138  xrsmopn  20369  recld2  20371  icccmplem1  20379  icccmplem2  20380  icccmp  20382  reconnlem2  20384  lebnumlem3  20515  lebnum  20516  xlebnum  20517  lebnumii  20518  nmhmcn  20655  cfilfval  20755  caubl  20798  caublcls  20799  bcthlem1  20815  bcth  20820  ovolfiniun  20964  ovoliunlem3  20967  ovoliun  20968  ovoliun2  20969  ovoliunnul  20970  voliunlem3  21013  dyadmax  21058  dyadmbllem  21059  dyadmbl  21060  opnmbllem  21061  ellimc2  21332  limcnlp  21333  ellimc3  21334  limcflf  21336  limciun  21349  cpnord  21389  lhop  21468  xrlimcnp  22342  cvxcl  22358  dchrval  22553  isssp  24090  ubthlem1  24239  shmodi  24761  chsupid  24783  chsscon3  24871  spansncvi  25023  mdslmd1lem3  25699  mdslmd1lem4  25700  mdsymlem5  25779  dmdbr5ati  25794  dmdbr6ati  25795  dmdbr7ati  25796  ssiun2sf  25878  fpwrelmapffslem  26000  tpr2rico  26311  pnfneige0  26350  rrhre  26416  dya2icoseg2  26662  omsfval  26678  eulerpartlemt0  26721  eulerpartgbij  26724  eulerpartlemr  26726  eulerpartlemgs2  26732  eulerpartlemn  26733  eulerpart  26734  kur14  27073  cvmliftlem15  27156  cvmlift2lem12  27172  cvmlift2lem13  27173  relexpdm  27306  relexprn  27307  rtrclreclem.min  27318  dfrtrcl2  27319  dfpo2  27534  preddowncl  27626  trpredlem1  27660  trpredmintr  27664  wrecseq123  27687  wfrlem1  27693  wfrlem3  27695  wfrlem9  27701  wfrlem15  27707  frrlem1  27737  frrlem4  27740  frrlem5e  27745  nobndup  27810  nobnddown  27811  nofulllem5  27816  opnmbllem0  28398  mblfinlem1  28399  mblfinlem2  28400  mblfinlem3  28401  ovoliunnfl  28404  ex-ovoliunnfl  28405  voliunnfl  28406  opnrebl  28486  opnrebl2  28487  ivthALT  28501  neibastop2lem  28552  fnemeet1  28558  filnetlem1  28570  filnetlem4  28573  totbndbnd  28659  heibor1lem  28679  heiborlem10  28690  scottexf  28951  scott0f  28952  ismrcd1  29005  nacsfix  29019  setindtr  29344  hbtlem6  29456  frgraunss  30558  frgra1v  30561  frgra2v  30562  frgra3vlem1  30563  frgra3vlem2  30564  frgra3v  30565  4cycl2vnunb  30580  n4cyclfrgra  30581  fsuppmapnn0fiub0  30770  bnj517  31807  bnj1014  31882  bnj1015  31883  bnj1123  31906  bnj1125  31912  bnj1450  31970  bnj1452  31972  lcv1  32579  lfl1dim  32659  lfl1dim2N  32660  paddasslem17  33373  dihglblem6  34878  dochvalr  34895  dochord3  34910  lpolconN  35025  lcfls1lem  35072  mapdffval  35164  mapdfval  35165  mapdsn2  35180  mapd0  35203  lspindp5  35308  mapdh8ab  35315
  Copyright terms: Public domain W3C validator