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

Theorem sseq1d 3524
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 3518 . 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 1374    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-in 3476  df-ss 3483
This theorem is referenced by:  sseq12d  3526  eqsstrd  3531  snssg  4153  ssiun2s  4362  disjxiun  4437  treq  4539  funimass1  5652  feq1  5704  fvmptss  5949  fvimacnvi  5986  fvimacnvALT  5991  fnsuppresOLD  6112  knatar  6232  ovmptss  6854  fnsuppres  6917  imacosupp  6930  oaordi  7185  oaword2  7192  oawordeulem  7193  omword1  7212  oewordri  7231  oeordsuc  7233  nnaordi  7257  nnawordex  7276  ereq1  7308  elpm2r  7426  inficl  7874  fipwss  7878  dffi3  7880  hartogslem1  7956  inf3lema  8030  inf3lemd  8033  cantnfle  8079  cantnflem2  8098  cantnfleOLD  8109  trcl  8148  tcmin  8161  rankr1ai  8205  rankxplim  8286  scottex  8292  scott0  8293  scottexs  8294  scott0s  8295  karden  8302  cardne  8335  cardaleph  8459  ackbij2  8612  cflim2  8632  cfslb  8635  coftr  8642  fin23lem15  8703  fin23lem32  8713  fin23lem34  8715  fin23lem35  8716  fin23lem36  8717  fin23lem41  8721  isf32lem1  8722  itunitc1  8789  axdc3lem2  8820  ttukeylem1  8878  fpwwe2cbv  8997  fpwwe2lem2  8999  fpwwe2  9010  fpwwecbv  9011  fpwwelem  9012  canthwelem  9017  canthwe  9018  wunex2  9105  wuncval2  9114  eltsk2g  9118  tskpwss  9119  inar1  9142  grothpw  9193  grothpwex  9194  axgroth6  9195  grothac  9197  peano5uzti  10939  fsuppmapnn0fiub0  12055  lo1o1  13304  o1lo1  13309  o1lo12  13310  lo1eq  13340  rlimeq  13341  isercoll  13439  prmreclem4  14285  vdwmc  14344  vdwlem1  14347  vdwlem2  14348  vdwlem12  14358  vdwlem13  14359  ramval  14374  ramz2  14390  ramub1lem1  14392  isacs2  14897  isacs1i  14901  mreacs  14902  acsfn  14903  rescabs  15052  ipole  15634  ipodrsima  15641  isacs5  15648  symgsssg  16281  psgnunilem5  16308  sylow1  16412  efgval2  16531  efgsfo  16546  frgpuplem  16579  gsumzf1o  16701  gsumzmhm  16741  gsumzoppg  16751  dprdcntz  16825  islbs2  17576  frlmssuvc1  18585  frlmssuvc2  18586  frlmssuvc1OLD  18587  frlmssuvc2OLD  18588  frlmsslsp  18589  frlmsslspOLD  18590  pptbas  19268  pnfnei  19480  mnfnei  19481  iscnp  19497  iscnp4  19523  cnntr  19535  cnconst2  19543  cnpresti  19548  cnprest  19549  isreg  19592  isnrm  19595  isnrm2  19618  perfcls  19625  isreg2  19637  hauscmplem  19665  1stcfb  19705  1stcelcls  19721  1stccnp  19722  txbas  19796  ptbasfi  19810  xkoopn  19818  xkoccn  19848  txcnp  19849  ptcnplem  19850  txdis  19861  txdis1cn  19864  txtube  19869  txkgen  19881  xkohaus  19882  xkoptsub  19883  xkoco1cn  19886  xkoco2cn  19887  xkococnlem  19888  xkococn  19889  xkoinjcn  19916  kqreglem1  19970  kqreglem2  19971  kqnrmlem1  19972  kqnrmlem2  19973  reghmph  20022  nrmhmph  20023  trfil2  20116  ufileu  20148  elfm  20176  elfm2  20177  elfm3  20179  imaelfm  20180  rnelfm  20182  fmfnfmlem2  20184  fmfnfmlem4  20186  fmco  20190  elflim2  20193  flffbas  20224  lmflf  20234  txflf  20235  fclscf  20254  flimfnfcls  20257  cnextcn  20295  symgtgp  20328  ghmcnp  20341  divstgplem  20347  eltsms  20359  ustval  20433  ust0  20450  trust  20460  utoptop  20465  restutop  20468  restutopopn  20469  utopsnneiplem  20478  ucncn  20516  fmucnd  20523  cfilufg  20524  trcfilu  20525  neipcfilu  20527  blssps  20655  blss  20656  ssblex  20659  blin2  20660  metss2  20743  metrest  20755  metcnp3  20771  metustexhalfOLD  20794  metustexhalf  20795  metustblOLD  20811  metustbl  20812  metutopOLD  20813  psmetutop  20814  xrsmopn  21045  recld2  21047  icccmplem1  21055  icccmplem2  21056  icccmp  21058  reconnlem2  21060  lebnumlem3  21191  lebnum  21192  xlebnum  21193  lebnumii  21194  nmhmcn  21331  cfilfval  21431  caubl  21474  caublcls  21475  bcthlem1  21491  bcth  21496  ovolfiniun  21640  ovoliunlem3  21643  ovoliun  21644  ovoliun2  21645  ovoliunnul  21646  voliunlem3  21690  dyadmax  21735  dyadmbllem  21736  dyadmbl  21737  opnmbllem  21738  ellimc2  22009  limcnlp  22010  ellimc3  22011  limcflf  22013  limciun  22026  cpnord  22066  lhop  22145  xrlimcnp  23019  cvxcl  23035  dchrval  23230  isssp  25163  ubthlem1  25312  shmodi  25834  chsupid  25856  chsscon3  25944  spansncvi  26096  mdslmd1lem3  26772  mdslmd1lem4  26773  mdsymlem5  26852  dmdbr5ati  26867  dmdbr6ati  26868  dmdbr7ati  26869  ssiun2sf  26950  fpwrelmapffslem  27077  txomap  27350  tpr2rico  27380  pnfneige0  27419  rrhre  27485  dya2icoseg2  27739  omsfval  27755  eulerpartlemt0  27798  eulerpartgbij  27801  eulerpartlemr  27803  eulerpartlemgs2  27809  eulerpartlemn  27810  eulerpart  27811  kur14  28150  cvmliftlem15  28233  cvmlift2lem12  28249  cvmlift2lem13  28250  relexpdm  28383  relexprn  28384  rtrclreclem.min  28395  dfrtrcl2  28396  dfpo2  28611  preddowncl  28703  trpredlem1  28737  trpredmintr  28741  wrecseq123  28764  wfrlem1  28770  wfrlem3  28772  wfrlem9  28778  wfrlem15  28784  frrlem1  28814  frrlem4  28817  frrlem5e  28822  nobndup  28887  nobnddown  28888  nofulllem5  28893  opnmbllem0  29478  mblfinlem1  29479  mblfinlem2  29480  mblfinlem3  29481  ovoliunnfl  29484  ex-ovoliunnfl  29485  voliunnfl  29486  opnrebl  29566  opnrebl2  29567  ivthALT  29581  neibastop2lem  29632  fnemeet1  29638  filnetlem1  29650  filnetlem4  29653  totbndbnd  29739  heibor1lem  29759  heiborlem10  29770  scottexf  30031  scott0f  30032  ismrcd1  30085  nacsfix  30099  setindtr  30423  hbtlem6  30535  fnresdmss  30840  icccncfext  31045  dvmulcncf  31074  dvdivcncf  31076  fourierdlem41  31267  fourierdlem89  31315  fourierdlem91  31317  frgraunss  31713  frgra1v  31716  frgra2v  31717  frgra3vlem1  31718  frgra3vlem2  31719  frgra3v  31720  4cycl2vnunb  31735  n4cyclfrgra  31736  bnj517  32897  bnj1014  32972  bnj1015  32973  bnj1123  32996  bnj1125  33002  bnj1450  33060  bnj1452  33062  lcv1  33713  lfl1dim  33793  lfl1dim2N  33794  paddasslem17  34507  dihglblem6  36012  dochvalr  36029  dochord3  36044  lpolconN  36159  lcfls1lem  36206  mapdffval  36298  mapdfval  36299  mapdsn2  36314  mapd0  36337  lspindp5  36442  mapdh8ab  36449
  Copyright terms: Public domain W3C validator