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

Theorem sseq1d 3526
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 3520 . 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 1395    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3478  df-ss 3485
This theorem is referenced by:  sseq12d  3528  eqsstrd  3533  snssg  4165  ssiun2s  4376  disjxiun  4453  treq  4556  funimass1  5667  feq1  5719  fvmptss  5965  fvimacnvi  6002  fvimacnvALT  6007  fnsuppresOLD  6132  knatar  6254  ovmptss  6880  fnsuppres  6945  imacosupp  6958  oaordi  7213  oaword2  7220  oawordeulem  7221  omword1  7240  oewordri  7259  oeordsuc  7261  nnaordi  7285  nnawordex  7304  ereq1  7336  elpm2r  7455  inficl  7903  fipwss  7907  dffi3  7909  hartogslem1  7985  inf3lema  8058  inf3lemd  8061  cantnfle  8107  cantnflem2  8126  cantnfleOLD  8137  trcl  8176  tcmin  8189  rankr1ai  8233  rankxplim  8314  scottex  8320  scott0  8321  scottexs  8322  scott0s  8323  karden  8330  cardne  8363  cardaleph  8487  ackbij2  8640  cflim2  8660  cfslb  8663  coftr  8670  fin23lem15  8731  fin23lem32  8741  fin23lem34  8743  fin23lem35  8744  fin23lem36  8745  fin23lem41  8749  isf32lem1  8750  itunitc1  8817  axdc3lem2  8848  ttukeylem1  8906  fpwwe2cbv  9025  fpwwe2lem2  9027  fpwwe2  9038  fpwwecbv  9039  fpwwelem  9040  canthwelem  9045  canthwe  9046  wunex2  9133  wuncval2  9142  eltsk2g  9146  tskpwss  9147  inar1  9170  grothpw  9221  grothpwex  9222  axgroth6  9223  grothac  9225  peano5uzti  10973  fsuppmapnn0fiub0  12102  lo1o1  13367  o1lo1  13372  o1lo12  13373  lo1eq  13403  rlimeq  13404  isercoll  13502  prmreclem4  14449  vdwmc  14508  vdwlem1  14511  vdwlem2  14512  vdwlem12  14522  vdwlem13  14523  ramval  14538  ramz2  14554  ramub1lem1  14556  isacs2  15070  isacs1i  15074  mreacs  15075  acsfn  15076  rescabs  15249  ipole  15915  ipodrsima  15922  isacs5  15929  symgsssg  16619  psgnunilem5  16646  sylow1  16750  efgval2  16869  efgsfo  16884  frgpuplem  16917  gsumzf1o  17044  gsumzoppg  17094  dprdcntz  17168  islbs2  17927  frlmssuvc1  18952  frlmssuvc2  18953  frlmssuvc1OLD  18954  frlmssuvc2OLD  18955  frlmsslsp  18956  frlmsslspOLD  18957  pptbas  19636  pnfnei  19848  mnfnei  19849  iscnp  19865  iscnp4  19891  cnntr  19903  cnconst2  19911  cnpresti  19916  cnprest  19917  isreg  19960  isnrm  19963  isnrm2  19986  perfcls  19993  isreg2  20005  hauscmplem  20033  1stcfb  20072  1stcelcls  20088  1stccnp  20089  txbas  20194  ptbasfi  20208  xkoopn  20216  xkoccn  20246  txcnp  20247  ptcnplem  20248  txdis  20259  txdis1cn  20262  txtube  20267  txkgen  20279  xkohaus  20280  xkoptsub  20281  xkoco1cn  20284  xkoco2cn  20285  xkococnlem  20286  xkococn  20287  xkoinjcn  20314  kqreglem1  20368  kqreglem2  20369  kqnrmlem1  20370  kqnrmlem2  20371  reghmph  20420  nrmhmph  20421  trfil2  20514  ufileu  20546  elfm  20574  elfm2  20575  elfm3  20577  imaelfm  20578  rnelfm  20580  fmfnfmlem2  20582  fmfnfmlem4  20584  fmco  20588  elflim2  20591  flffbas  20622  lmflf  20632  txflf  20633  fclscf  20652  flimfnfcls  20655  cnextcn  20693  symgtgp  20726  ghmcnp  20739  qustgplem  20745  eltsms  20757  ustval  20831  ust0  20848  trust  20858  utoptop  20863  restutop  20866  restutopopn  20867  utopsnneiplem  20876  ucncn  20914  fmucnd  20921  cfilufg  20922  trcfilu  20923  neipcfilu  20925  blssps  21053  blss  21054  ssblex  21057  blin2  21058  metss2  21141  metrest  21153  metcnp3  21169  metustexhalfOLD  21192  metustexhalf  21193  metustblOLD  21209  metustbl  21210  metutopOLD  21211  psmetutop  21212  xrsmopn  21443  recld2  21445  icccmplem1  21453  icccmplem2  21454  icccmp  21456  reconnlem2  21458  lebnumlem3  21589  lebnum  21590  xlebnum  21591  lebnumii  21592  nmhmcn  21729  cfilfval  21829  caubl  21872  caublcls  21873  bcthlem1  21889  bcth  21894  ovolfiniun  22038  ovoliunlem3  22041  ovoliun  22042  ovoliun2  22043  ovoliunnul  22044  voliunlem3  22088  dyadmax  22133  dyadmbllem  22134  dyadmbl  22135  opnmbllem  22136  ellimc2  22407  limcnlp  22408  ellimc3  22409  limcflf  22411  limciun  22424  cpnord  22464  lhop  22543  xrlimcnp  23424  cvxcl  23440  dchrval  23635  frgraunss  25122  frgra1v  25125  frgra2v  25126  frgra3vlem1  25127  frgra3vlem2  25128  frgra3v  25129  4cycl2vnunb  25144  n4cyclfrgra  25145  isssp  25764  ubthlem1  25913  shmodi  26435  chsupid  26457  chsscon3  26545  spansncvi  26697  mdslmd1lem3  27373  mdslmd1lem4  27374  mdsymlem5  27453  dmdbr5ati  27468  dmdbr6ati  27469  dmdbr7ati  27470  ssiun2sf  27565  fpwrelmapffslem  27712  txomap  27998  locfinreflem  28004  tpr2rico  28055  pnfneige0  28094  rrhre  28160  dya2icoseg2  28422  omsfval  28438  eulerpartlemt0  28505  eulerpartgbij  28508  eulerpartlemr  28510  eulerpartlemgs2  28516  eulerpartlemn  28517  eulerpart  28518  kur14  28857  cvmliftlem15  28940  cvmlift2lem12  28956  cvmlift2lem13  28957  mclsval  29120  mclsax  29126  mclsppslem  29140  relexpnndm  29266  rtrclreclem.min  29288  dfrtrcl2  29289  dfpo2  29402  preddowncl  29493  trpredlem1  29527  trpredmintr  29531  wrecseq123  29554  wfrlem1  29560  wfrlem3  29562  wfrlem9  29568  wfrlem15  29574  frrlem1  29604  frrlem4  29607  frrlem5e  29612  nobndup  29677  nobnddown  29678  nofulllem5  29683  opnmbllem0  30255  mblfinlem1  30256  mblfinlem2  30257  mblfinlem3  30258  ovoliunnfl  30261  ex-ovoliunnfl  30262  voliunnfl  30263  opnrebl  30343  opnrebl2  30344  ivthALT  30358  neibastop2lem  30383  fnemeet1  30389  filnetlem1  30401  filnetlem4  30404  totbndbnd  30490  heibor1lem  30510  heiborlem10  30521  scottexf  30781  scott0f  30782  ismrcd1  30835  nacsfix  30849  setindtr  31170  hbtlem6  31282  icccncfext  31893  fourierdlem41  32133  dfrngc2  32924  bnj517  34086  bnj1014  34161  bnj1015  34162  bnj1123  34185  bnj1125  34191  bnj1450  34249  bnj1452  34251  lcv1  34909  lfl1dim  34989  lfl1dim2N  34990  paddasslem17  35703  dihglblem6  37210  dochvalr  37227  dochord3  37242  lpolconN  37357  lcfls1lem  37404  mapdffval  37496  mapdfval  37497  mapdsn2  37512  mapd0  37535  lspindp5  37640  mapdh8ab  37647
  Copyright terms: Public domain W3C validator