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

Theorem sseq1d 3469
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 3463 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2syl 17 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1405    C_ wss 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3421  df-ss 3428
This theorem is referenced by:  sseq12d  3471  eqsstrd  3476  snssg  4105  ssiun2s  4315  disjxiun  4392  treq  4495  preddowncl  5394  funimass1  5642  feq1  5696  fvmptss  5942  fvimacnvi  5979  fvimacnvALT  5984  fnsuppresOLD  6113  knatar  6236  ovmptss  6865  fnsuppres  6930  imacosupp  6943  wrecseq123  7014  wfrlem1  7020  wfrlem3  7022  wfrdmcl  7029  wfrlem15  7035  wfrlem17  7037  dfrecs3  7076  oaordi  7232  oaword2  7239  oawordeulem  7240  omword1  7259  oewordri  7278  oeordsuc  7280  nnaordi  7304  nnawordex  7323  ereq1  7355  elpm2r  7474  inficl  7919  fipwss  7923  dffi3  7925  hartogslem1  8001  inf3lema  8074  inf3lemd  8077  cantnfle  8122  cantnflem2  8141  cantnfleOLD  8152  trcl  8191  tcmin  8204  rankr1ai  8248  rankxplim  8329  scottex  8335  scott0  8336  scottexs  8337  scott0s  8338  karden  8345  cardne  8378  cardaleph  8502  ackbij2  8655  cflim2  8675  cfslb  8678  coftr  8685  fin23lem15  8746  fin23lem32  8756  fin23lem34  8758  fin23lem35  8759  fin23lem36  8760  fin23lem41  8764  isf32lem1  8765  itunitc1  8832  axdc3lem2  8863  ttukeylem1  8921  fpwwe2cbv  9038  fpwwe2lem2  9040  fpwwe2  9051  fpwwecbv  9052  fpwwelem  9053  canthwelem  9058  canthwe  9059  wunex2  9146  wuncval2  9155  eltsk2g  9159  tskpwss  9160  inar1  9183  grothpw  9234  grothpwex  9235  axgroth6  9236  grothac  9238  peano5uzti  10993  fsuppmapnn0fiub0  12143  relexpnndm  13023  rtrclreclem4  13043  dfrtrcl2  13044  lo1o1  13504  o1lo1  13509  o1lo12  13510  lo1eq  13540  rlimeq  13541  isercoll  13639  prmreclem4  14646  vdwmc  14705  vdwlem1  14708  vdwlem2  14709  vdwlem12  14719  vdwlem13  14720  ramval  14735  ramz2  14751  ramub1lem1  14753  isacs2  15267  isacs1i  15271  mreacs  15272  acsfn  15273  rescabs  15446  ipole  16112  ipodrsima  16119  isacs5  16126  symgsssg  16816  psgnunilem5  16843  sylow1  16947  efgval2  17066  efgsfo  17081  frgpuplem  17114  gsumzf1o  17241  gsumzoppg  17290  dprdcntz  17361  islbs2  18120  frlmssuvc1  19121  frlmssuvc2  19122  frlmsslsp  19123  pptbas  19801  pnfnei  20014  mnfnei  20015  iscnp  20031  iscnp4  20057  cnntr  20069  cnconst2  20077  cnpresti  20082  cnprest  20083  isreg  20126  isnrm  20129  isnrm2  20152  perfcls  20159  isreg2  20171  hauscmplem  20199  1stcfb  20238  1stcelcls  20254  1stccnp  20255  txbas  20360  ptbasfi  20374  xkoopn  20382  xkoccn  20412  txcnp  20413  ptcnplem  20414  txdis  20425  txdis1cn  20428  txtube  20433  txkgen  20445  xkohaus  20446  xkoptsub  20447  xkoco1cn  20450  xkoco2cn  20451  xkococnlem  20452  xkococn  20453  xkoinjcn  20480  kqreglem1  20534  kqreglem2  20535  kqnrmlem1  20536  kqnrmlem2  20537  reghmph  20586  nrmhmph  20587  trfil2  20680  ufileu  20712  elfm  20740  elfm2  20741  elfm3  20743  imaelfm  20744  rnelfm  20746  fmfnfmlem2  20748  fmfnfmlem4  20750  fmco  20754  elflim2  20757  flffbas  20788  lmflf  20798  txflf  20799  fclscf  20818  flimfnfcls  20821  cnextcn  20859  symgtgp  20892  ghmcnp  20905  qustgplem  20911  eltsms  20923  ustval  20997  ust0  21014  trust  21024  utoptop  21029  restutop  21032  restutopopn  21033  utopsnneiplem  21042  ucncn  21080  fmucnd  21087  cfilufg  21088  trcfilu  21089  neipcfilu  21091  blssps  21219  blss  21220  ssblex  21223  blin2  21224  metss2  21307  metrest  21319  metcnp3  21335  metustexhalfOLD  21358  metustexhalf  21359  metustblOLD  21375  metustbl  21376  metutopOLD  21377  psmetutop  21378  xrsmopn  21609  recld2  21611  icccmplem1  21619  icccmplem2  21620  icccmp  21622  reconnlem2  21624  lebnumlem3  21755  lebnum  21756  xlebnum  21757  lebnumii  21758  nmhmcn  21895  cfilfval  21995  caubl  22038  caublcls  22039  bcthlem1  22055  bcth  22060  ovolfiniun  22204  ovoliunlem3  22207  ovoliun  22208  ovoliun2  22209  ovoliunnul  22210  voliunlem3  22254  dyadmax  22299  dyadmbllem  22300  dyadmbl  22301  opnmbllem  22302  ellimc2  22573  limcnlp  22574  ellimc3  22575  limcflf  22577  limciun  22590  cpnord  22630  lhop  22709  xrlimcnp  23624  cvxcl  23640  dchrval  23890  frgraunss  25412  frgra1v  25415  frgra2v  25416  frgra3vlem1  25417  frgra3vlem2  25418  frgra3v  25419  4cycl2vnunb  25434  n4cyclfrgra  25435  isssp  26051  ubthlem1  26200  shmodi  26722  chsupid  26744  chsscon3  26832  spansncvi  26984  mdslmd1lem3  27659  mdslmd1lem4  27660  mdsymlem5  27739  dmdbr5ati  27754  dmdbr6ati  27755  dmdbr7ati  27756  ssiun2sf  27856  fpwrelmapffslem  28002  txomap  28290  locfinreflem  28296  tpr2rico  28347  pnfneige0  28386  rrhre  28451  dya2icoseg2  28726  omsfval  28742  eulerpartlemt0  28814  eulerpartgbij  28817  eulerpartlemr  28819  eulerpartlemgs2  28825  eulerpartlemn  28826  eulerpart  28827  bnj517  29270  bnj1014  29345  bnj1015  29346  bnj1123  29369  bnj1125  29375  bnj1450  29433  bnj1452  29435  kur14  29513  cvmliftlem15  29595  cvmlift2lem12  29611  cvmlift2lem13  29612  mclsval  29775  mclsax  29781  mclsppslem  29795  dfpo2  29968  trpredlem1  30041  trpredmintr  30045  frrlem1  30087  frrlem4  30090  frrlem5e  30095  nobndup  30160  nobnddown  30161  nofulllem5  30166  opnrebl  30548  opnrebl2  30549  ivthALT  30563  neibastop2lem  30588  fnemeet1  30594  filnetlem1  30606  filnetlem4  30609  opnmbllem0  31422  mblfinlem1  31423  mblfinlem2  31424  mblfinlem3  31425  ovoliunnfl  31428  ex-ovoliunnfl  31429  voliunnfl  31430  totbndbnd  31567  heibor1lem  31587  heiborlem10  31598  scottexf  31858  scott0f  31859  lcv1  32059  lfl1dim  32139  lfl1dim2N  32140  paddasslem17  32853  dihglblem6  34360  dochvalr  34377  dochord3  34392  lpolconN  34507  lcfls1lem  34554  mapdffval  34646  mapdfval  34647  mapdsn2  34662  mapd0  34685  lspindp5  34790  mapdh8ab  34797  ismrcd1  34992  nacsfix  35006  setindtr  35328  hbtlem6  35442  iunrelexpmin1  35687  iunrelexpmin2  35691  relexp0a  35695  cotrcltrcl  35704  trclimalb2  35705  cotrclrcl  35721  sbcheg  35759  icccncfext  37058  fourierdlem41  37298  dfrngc2  38291
  Copyright terms: Public domain W3C validator