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

Theorem sseq1d 3239
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 3233 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2syl 15 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1633    C_ wss 3186
This theorem is referenced by:  sseq12d  3241  eqsstrd  3246  snssg  3788  ssiun2s  3983  disjxiun  4057  treq  4156  dmxpss  5144  iotassuni  5272  funimass1  5362  feq1  5412  fvmptss  5647  fvimacnvi  5677  fvimacnvALT  5682  fnsuppres  5773  knatar  5899  ovmptss  6242  tposss  6277  oaordi  6586  oaword2  6593  oawordeulem  6594  omwordri  6612  omword1  6613  oewordri  6632  oeordsuc  6634  nnaordi  6658  nnawordex  6677  ereq1  6709  elpm2r  6831  map0e  6848  sbthlem5  7018  fodomr  7055  inficl  7223  fipwuni  7224  fipwss  7227  dffi3  7229  ordtypelem6  7283  hartogslem1  7302  inf3lema  7370  inf3lemd  7373  cantnfle  7417  cantnflem2  7437  trcl  7455  tcmin  7471  rankr1ai  7515  rankxplim  7594  scottex  7600  scott0  7601  scottexs  7602  scott0s  7603  karden  7610  cardne  7643  cardaleph  7761  ackbij2  7914  cfub  7920  cflecard  7924  cfle  7925  cflim2  7934  cfslb  7937  coftr  7944  fin23lem15  8005  fin23lem29  8012  fin23lem32  8015  fin23lem34  8017  fin23lem35  8018  fin23lem36  8019  fin23lem41  8023  isf32lem1  8024  compsscnvlem  8041  itunitc1  8091  axdc3lem2  8122  ttukeylem1  8181  fpwwe2cbv  8297  fpwwe2lem2  8299  fpwwe2  8310  fpwwecbv  8311  fpwwelem  8312  canthwelem  8317  canthwe  8318  wunex2  8405  wuncval2  8414  eltsk2g  8418  tskpwss  8419  inar1  8442  grur1a  8486  grothpw  8493  grothpwex  8494  axgroth6  8495  grothac  8497  peano5uzti  10148  lo1o1  12053  o1lo1  12058  o1lo12  12059  lo1eq  12089  rlimeq  12090  isercoll  12188  sadcaddlem  12695  sadcl  12700  smupvallem  12721  smucl  12722  prmreclem4  13013  vdwmc  13072  vdwlem1  13075  vdwlem2  13076  vdwlem12  13086  vdwlem13  13087  ramval  13102  ramz2  13118  ramub1lem1  13120  strfvss  13213  prdsless  13411  isacs2  13604  isacs1i  13608  mreacs  13609  acsfn  13610  rescabs  13759  ipole  14310  ipodrsima  14317  isacs5  14324  sylow1  14963  efgval2  15082  efgsfo  15097  frgpuplem  15130  dprdcntz  15292  islbs2  15956  resspsrbas  16208  resspsrvsca  16211  subrgpsr  16212  ressmplbas  16249  subrgmpl  16253  ressply1bas  16356  cssss  16641  basdif0  16747  pptbas  16801  ordtbas2  16977  ordtbas  16978  pnfnei  17006  mnfnei  17007  iscnp  17023  cnclsi  17057  cncls  17059  cnntr  17060  cnconst2  17067  cnpresti  17072  cnprest  17073  isreg  17116  isnrm  17119  isnrm2  17142  perfcls  17149  isreg2  17161  hauscmplem  17189  cmpfi  17191  1stcfb  17227  1stcelcls  17243  1stccnp  17244  txbas  17318  ptbasfi  17332  xkoopn  17340  txss12  17356  txbasval  17357  xkoccn  17369  txcnp  17370  ptcnplem  17371  prdstopn  17378  txdis  17382  txdis1cn  17385  txtube  17390  txkgen  17402  xkohaus  17403  xkoptsub  17404  xkoco1cn  17407  xkoco2cn  17408  xkococnlem  17409  xkococn  17410  xkoinjcn  17437  kqsat  17478  kqcldsat  17480  kqreglem1  17488  kqreglem2  17489  kqnrmlem1  17490  kqnrmlem2  17491  reghmph  17540  nrmhmph  17541  trfil2  17634  ufileu  17666  elfm  17694  elfm2  17695  elfm3  17697  imaelfm  17698  rnelfm  17700  fmfnfmlem2  17702  fmfnfmlem4  17704  fmco  17708  elflim2  17711  flffbas  17742  lmflf  17752  txflf  17753  fclscf  17772  flimfnfcls  17775  symgtgp  17836  ghmcnp  17849  divstgplem  17855  eltsms  17867  blss  18024  ssblex  18026  blin2  18027  setsmstopn  18076  metss2  18110  metrest  18122  metcnp3  18138  tngtopn  18218  xrsmopn  18370  recld2  18372  icccmplem1  18379  icccmplem2  18380  icccmp  18382  reconnlem2  18384  metdstri  18407  lebnumlem3  18514  lebnum  18515  xlebnum  18516  lebnumii  18517  nmhmcn  18654  cphsubrglem  18666  tchcph  18720  cfilfval  18743  caubl  18786  caublcls  18787  bcthlem1  18799  bcth  18804  ovolfiniun  18913  ovoliunlem3  18916  ovoliun  18917  ovoliun2  18918  ovoliunnul  18919  voliunlem3  18962  uniioombllem2  18991  dyadmax  19006  dyadmbllem  19007  dyadmbl  19008  opnmbllem  19009  ellimc2  19280  limcnlp  19281  ellimc3  19282  limcflf  19284  limciun  19297  cpnord  19337  lhop  19416  dvfsumle  19421  dvfsumabs  19423  xrlimcnp  20316  cvxcl  20332  dchrval  20526  dchrelbas2  20529  subgornss  21026  isssp  21355  ubthlem1  21504  ocsh  21917  shmodi  22024  chsupid  22046  chsupsn  22047  chsscon3  22134  spansncvi  22286  pj3i  22843  mdslmd1lem3  22962  mdslmd1lem4  22963  mdsymlem5  23042  sumdmdlem2  23054  dmdbr5ati  23057  dmdbr6ati  23058  dmdbr7ati  23059  ssiun2sf  23153  tpr2rico  23379  pnfneige0  23405  ustval  23419  ust0  23432  trust  23441  utoptop  23446  restutop  23448  restutopopn  23449  fmucnd  23484  metustexhalf  23498  metustbl  23508  metutop  23509  dya2icoseg2  23802  kur14lem1  24021  kur14  24031  cvmliftlem15  24113  cvmlift2lem12  24129  cvmlift2lem13  24130  relexpdm  24316  relexprn  24317  rtrclreclem.min  24328  dfrtrcl2  24329  dfpo2  24497  preddowncl  24581  trpredlem1  24615  trpredmintr  24619  wfrlem1  24641  wfrlem3  24643  wfrlem9  24649  wfrlem15  24655  tfrALTlem  24661  frrlem1  24666  frrlem4  24669  frrlem5e  24674  nobndup  24739  nobnddown  24740  nofulllem5  24745  bpolyval  25170  ovoliunnfl  25315  ex-ovoliunnfl  25316  opnrebl  25384  opnrebl2  25385  ivthALT  25407  neibastop2lem  25458  fnemeet1  25464  filnetlem1  25476  filnetlem4  25479  isbnd3  25656  totbndbnd  25661  heibor1lem  25681  heiborlem10  25692  ismrcd1  25921  nacsfix  25935  setindtr  26265  frlmssuvc1  26394  frlmssuvc2  26395  frlmsslsp  26396  hbtlem6  26481  symgsssg  26556  psgnunilem5  26565  frgraunss  27587  frgra1v  27590  frgra2v  27591  frgra3vlem1  27592  frgra3vlem2  27593  frgra3v  27594  4cycl2vnunb  27609  n4cyclfrgra  27610  bnj517  28428  bnj1014  28503  bnj1015  28504  bnj1123  28527  bnj1125  28533  bnj1450  28591  bnj1452  28593  lcv1  29049  lfl1dim  29129  lfl1dim2N  29130  paddasslem17  29843  dihglblem6  31348  dochvalr  31365  dochord3  31380  lpolconN  31495  lcfls1lem  31542  mapdffval  31634  mapdfval  31635  mapdsn2  31650  mapd0  31673  lspindp5  31778  mapdh8ab  31785
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-in 3193  df-ss 3200
  Copyright terms: Public domain W3C validator