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

Theorem sseq1d 3491
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 3485 . 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 187    = wceq 1437    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  sseq12d  3493  eqsstrd  3498  snssg  4130  ssiun2s  4340  disjxiun  4417  treq  4521  preddowncl  5423  funimass1  5671  feq1  5725  fvmptss  5971  fvimacnvi  6008  fvimacnvALT  6013  knatar  6260  ovmptss  6885  fnsuppres  6950  imacosupp  6963  wrecseq123  7034  wfrlem1  7040  wfrlem3  7042  wfrdmcl  7049  wfrlem15  7055  wfrlem17  7057  dfrecs3  7096  oaordi  7252  oaword2  7259  oawordeulem  7260  omword1  7279  oewordri  7298  oeordsuc  7300  nnaordi  7324  nnawordex  7343  ereq1  7375  elpm2r  7494  inficl  7942  fipwss  7946  dffi3  7948  hartogslem1  8060  inf3lema  8132  inf3lemd  8135  cantnfle  8178  cantnflem2  8197  trcl  8214  tcmin  8227  rankr1ai  8271  rankxplim  8352  scottex  8358  scott0  8359  scottexs  8360  scott0s  8361  karden  8368  cardne  8401  cardaleph  8521  ackbij2  8674  cflim2  8694  cfslb  8697  coftr  8704  fin23lem15  8765  fin23lem32  8775  fin23lem34  8777  fin23lem35  8778  fin23lem36  8779  fin23lem41  8783  isf32lem1  8784  itunitc1  8851  axdc3lem2  8882  ttukeylem1  8940  fpwwe2cbv  9056  fpwwe2lem2  9058  fpwwe2  9069  fpwwecbv  9070  fpwwelem  9071  canthwelem  9076  canthwe  9077  wunex2  9164  wuncval2  9173  eltsk2g  9177  tskpwss  9178  inar1  9201  grothpw  9252  grothpwex  9253  axgroth6  9254  grothac  9256  peano5uzti  11026  fsuppmapnn0fiub0  12205  relexpnndm  13093  rtrclreclem4  13113  dfrtrcl2  13114  lo1o1  13584  o1lo1  13589  o1lo12  13590  lo1eq  13620  rlimeq  13621  isercoll  13719  prmreclem4  14851  vdwmc  14916  vdwlem1  14919  vdwlem2  14920  vdwlem12  14930  vdwlem13  14931  ramval  14948  ramvalOLD  14949  ramz2  14970  ramub1lem1  14972  isacs2  15547  isacs1i  15551  mreacs  15552  acsfn  15553  rescabs  15726  ipole  16392  ipodrsima  16399  isacs5  16406  symgsssg  17096  psgnunilem5  17123  sylow1  17243  efgval2  17362  efgsfo  17377  frgpuplem  17410  gsumzf1o  17534  gsumzoppg  17565  dprdcntz  17628  islbs2  18365  frlmssuvc1  19339  frlmssuvc2  19340  frlmsslsp  19341  pptbas  20010  pnfnei  20223  mnfnei  20224  iscnp  20240  iscnp4  20266  cnntr  20278  cnconst2  20286  cnpresti  20291  cnprest  20292  isreg  20335  isnrm  20338  isnrm2  20361  perfcls  20368  isreg2  20380  hauscmplem  20408  1stcfb  20447  1stcelcls  20463  1stccnp  20464  txbas  20569  ptbasfi  20583  xkoopn  20591  xkoccn  20621  txcnp  20622  ptcnplem  20623  txdis  20634  txdis1cn  20637  txtube  20642  txkgen  20654  xkohaus  20655  xkoptsub  20656  xkoco1cn  20659  xkoco2cn  20660  xkococnlem  20661  xkococn  20662  xkoinjcn  20689  kqreglem1  20743  kqreglem2  20744  kqnrmlem1  20745  kqnrmlem2  20746  reghmph  20795  nrmhmph  20796  trfil2  20889  ufileu  20921  elfm  20949  elfm2  20950  elfm3  20952  imaelfm  20953  rnelfm  20955  fmfnfmlem2  20957  fmfnfmlem4  20959  fmco  20963  elflim2  20966  flffbas  20997  lmflf  21007  txflf  21008  fclscf  21027  flimfnfcls  21030  cnextcn  21069  symgtgp  21103  ghmcnp  21116  qustgplem  21122  eltsms  21134  ustval  21204  ust0  21221  trust  21231  utoptop  21236  restutop  21239  restutopopn  21240  utopsnneiplem  21249  ucncn  21287  fmucnd  21294  cfilufg  21295  trcfilu  21296  neipcfilu  21298  blssps  21426  blss  21427  ssblex  21430  blin2  21431  metss2  21514  metrest  21526  metcnp3  21542  metustexhalf  21558  metustbl  21568  psmetutop  21569  xrsmopn  21817  recld2  21819  icccmplem1  21827  icccmplem2  21828  icccmp  21830  reconnlem2  21832  lebnumlem3  21978  lebnumlem3OLD  21981  lebnum  21982  xlebnum  21983  lebnumii  21984  nmhmcn  22121  cfilfval  22221  caubl  22264  caublcls  22265  bcthlem1  22279  bcth  22284  ovolfiniun  22441  ovoliunlem3  22444  ovoliun  22445  ovoliun2  22446  ovoliunnul  22447  voliunlem3  22492  dyadmax  22543  dyadmbllem  22544  dyadmbl  22545  opnmbllem  22546  ellimc2  22819  limcnlp  22820  ellimc3  22821  limcflf  22823  limciun  22836  cpnord  22876  lhop  22955  xrlimcnp  23881  cvxcl  23897  dchrval  24149  frgraunss  25709  frgra1v  25712  frgra2v  25713  frgra3vlem1  25714  frgra3vlem2  25715  frgra3v  25716  4cycl2vnunb  25731  n4cyclfrgra  25732  isssp  26349  ubthlem1  26498  shmodi  27029  chsupid  27051  chsscon3  27139  spansncvi  27291  mdslmd1lem3  27966  mdslmd1lem4  27967  mdsymlem5  28046  dmdbr5ati  28061  dmdbr6ati  28062  dmdbr7ati  28063  ssiun2sf  28164  fpwrelmapffslem  28311  txomap  28657  locfinreflem  28663  tpr2rico  28714  pnfneige0  28753  rrhre  28821  dya2icoseg2  29096  omsfval  29114  omsfvalOLD  29118  eulerpartlemt0  29198  eulerpartgbij  29201  eulerpartlemr  29203  eulerpartlemgs2  29209  eulerpartlemn  29210  eulerpart  29211  bnj517  29692  bnj1014  29767  bnj1015  29768  bnj1123  29791  bnj1125  29797  bnj1450  29855  bnj1452  29857  kur14  29935  cvmliftlem15  30017  cvmlift2lem12  30033  cvmlift2lem13  30034  mclsval  30197  mclsax  30203  mclsppslem  30217  dfpo2  30390  trpredlem1  30463  trpredmintr  30467  frrlem1  30509  frrlem4  30512  frrlem5e  30517  nobndup  30582  nobnddown  30583  nofulllem5  30588  opnrebl  30969  opnrebl2  30970  ivthALT  30984  neibastop2lem  31009  fnemeet1  31015  filnetlem1  31027  filnetlem4  31030  ptrecube  31854  poimirlem32  31886  opnmbllem0  31890  mblfinlem1  31891  mblfinlem2  31892  mblfinlem3  31893  ovoliunnfl  31896  ex-ovoliunnfl  31897  voliunnfl  31898  totbndbnd  32035  heibor1lem  32055  heiborlem10  32066  scottexf  32325  scott0f  32326  lcv1  32526  lfl1dim  32606  lfl1dim2N  32607  paddasslem17  33320  dihglblem6  34827  dochvalr  34844  dochord3  34859  lpolconN  34974  lcfls1lem  35021  mapdffval  35113  mapdfval  35114  mapdsn2  35129  mapd0  35152  lspindp5  35257  mapdh8ab  35264  ismrcd1  35459  nacsfix  35473  setindtr  35799  hbtlem6  35908  iunrelexpmin1  36160  iunrelexpmin2  36164  relexp0a  36168  cotrcltrcl  36177  trclimalb2  36178  cotrclrcl  36194  sbcheg  36232  ssnnf1octb  37320  icccncfext  37585  fourierdlem41  37831  iunopeqop  38707  ausgrumgri  38881  ausgrusgri  38882  dfrngc2  39246
  Copyright terms: Public domain W3C validator