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

Theorem sseqtrd 3480
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrd.1  |-  ( ph  ->  A  C_  B )
sseqtrd.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
sseqtrd  |-  ( ph  ->  A  C_  C )

Proof of Theorem sseqtrd
StepHypRef Expression
1 sseqtrd.1 . 2  |-  ( ph  ->  A  C_  B )
2 sseqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32sseq2d 3472 . 2  |-  ( ph  ->  ( A  C_  B  <->  A 
C_  C ) )
41, 3mpbid 215 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  sseqtr4d  3481  uniintsn  4286  oeeui  7334  nnaword2  7362  oaabs2  7377  erssxp  7417  fipwuni  7971  ordtypelem7  8070  cantnflem3  8227  cdainf  8653  ficardun2  8664  ackbij1lem12  8692  ackbij1b  8700  fin1a2lem13  8873  winafp  9153  ioodisj  11797  reltrclfv  13136  prodss  14056  vdwlem11  14996  mrcssv  15575  mrcsscl  15581  mrcuni  15582  mressmrcd  15588  mreexexlem2d  15606  mreexexlem3d  15607  mreexfidimd  15611  subcss2  15803  resssetc  16042  funcsetcres2  16043  estrres  16079  poslubdg  16450  ipodrsfi  16464  acsmap2d  16480  mrelatlub  16487  mreclatBAD  16488  subsubm  16659  subsubg  16895  oppglsm  17349  subglsm  17378  lsmdisj  17386  gsumval3  17596  dprdres  17716  dprdss  17717  dprd2da  17730  dmdprdsplit2lem  17733  ablfac1b  17758  pgpfac1lem3  17765  issubdrg  18088  subsubrg  18089  islssd  18214  lspun  18265  lspssp  18266  lsslsp  18293  lsmssspx  18366  lspabs2  18398  lspabs3  18399  lspsolvlem  18420  lbsextlem3  18438  mplbas2  18749  gsumply1subr  18882  qsssubdrg  19082  obselocv  19346  lsslindf  19443  tgcl  20040  basgen  20059  tgfiss  20062  bastop1  20064  bastop2  20065  clsss2  20143  elcls3  20154  topssnei  20195  neiptopnei  20203  neitr  20251  restcls  20252  restlp  20254  ordtrest2  20275  iscncl  20340  cncls2  20344  cncls  20345  cnntr  20346  lmcls  20373  tgcmp  20471  cmpcld  20472  uncmp  20473  hauscmplem  20476  cmpfi  20478  clscon  20500  2ndcsb  20519  2ndcctbss  20525  2ndcomap  20528  nllyrest  20556  1stckgenlem  20623  kgencn2  20627  kgen2cn  20629  ptbasfi  20651  txcld  20673  txcls  20674  txbasval  20676  neitx  20677  ptcld  20683  ptclsg  20685  txnlly  20707  hausdiag  20715  txkgen  20722  xkopt  20725  xkopjcn  20726  xkococnlem  20729  cnmpt1res  20746  cnmpt2res  20747  imasnopn  20760  imasncld  20761  imasncls  20762  qtopcld  20783  qtoprest  20787  qtopcmap  20789  kqcldsat  20803  kqreglem2  20812  kqnrmlem2  20814  hmeontr  20839  neifil  20950  fgtr  20960  trnei  20962  uffixfr  20993  uffix2  20994  uffixsn  20995  elflim  21041  flimclslem  21054  fclsopn  21084  fclscmpi  21099  fclscmp  21100  alexsubALTlem3  21119  alexsubALT  21121  ptcmplem3  21124  subgntr  21176  opnsubg  21177  clssubg  21178  clsnsg  21179  cldsubg  21180  tgpconcompeqg  21181  snclseqg  21185  tsmsgsum  21208  tsmsid  21209  tgptsmscld  21220  ustssco  21284  utop2nei  21320  utop3cls  21321  utopreg  21322  cnextucn  21373  ressprdsds  21441  lpbl  21573  met2ndci  21592  prdsxmslem2  21599  metustexhalf  21626  psmetutop  21637  tgioo  21869  metdstri  21923  metdseq0  21926  metdstriOLD  21938  metdseq0OLD  21941  xlebnum  22051  clsocv  22276  metelcls  22329  cmetss  22339  relcmpcmet  22341  cmpcmet  22342  minveclem4a  22427  minveclem4aOLD  22439  uniioovol  22592  uniioombllem3  22599  limcres  22897  dvbss  22912  perfdvf  22914  dvreslem  22920  dvres2lem  22921  dvcnp2  22930  dvaddbr  22948  dvmulbr  22949  dvcmulf  22955  dvcj  22960  dvnfre  22962  dvmptres2  22972  dvmptcmul  22974  dvmptntr  22981  dvlip2  23003  dvcnvrelem2  23026  ftc1cn  23051  taylfvallem1  23368  taylply2  23379  taylply  23380  dvtaylp  23381  dvntaylp  23382  dvntaylp0  23383  taylthlem1  23384  taylthlem2  23385  ulmdvlem3  23413  pserulm  23433  shsub2  27034  spanssoc  27058  shub2  27092  ococin  27117  ssjo  27156  chub2  27217  spanpr  27289  elnlfn  27637  mdslj1i  28028  mdslmd3i  28041  mdexchi  28044  chirredlem1  28099  atcvat3i  28105  mdsymlem1  28112  mdsymlem5  28116  imadifxp  28265  qtophaus  28714  locfinreflem  28718  fsumcvg4  28807  esum2d  28965  omsmon  29176  omssubadd  29178  omsmonOLD  29180  omssubaddOLD  29182  carsggect  29200  carsgclctun  29203  sitgclg  29225  eulerpartlemgf  29262  cvmscld  30046  cvmliftmolem1  30054  cvmlift2lem9  30084  cvmlift2lem11  30086  cvmlift3lem6  30097  nodense  30628  opnregcld  31036  ivthALT  31041  neibastop2  31067  fnemeet1  31072  fnejoin1  31074  poimirlem11  31997  poimirlem12  31998  poimirlem30  32016  ftc1cnnc  32062  sstotbnd  32153  ssbnd  32166  heibor1lem  32187  heiborlem3  32191  heibor  32199  lsmsat  32620  lssats  32624  lcvexchlem3  32648  lsatcvat3  32664  lkrscss  32710  lkrpssN  32775  pmod1i  33459  pclbtwnN  33508  pclunN  33509  pclss2polN  33532  pcl0N  33533  sspmaplubN  33536  paddunN  33538  pnonsingN  33544  pclfinclN  33561  osumcllem4N  33570  dia2dimlem13  34690  dvhopellsm  34731  dvadiaN  34742  dicelval1stN  34802  dicelval2nd  34803  dihssxp  34866  dihvalrel  34893  dochsscl  34982  dihoml4  34991  dochnoncon  35005  dvh3dim3N  35063  lcfrlem2  35157  lcfrlem5  35160  lcfr  35199  lcdlsp  35235  mapdsn  35255  mapdlsm  35278  mapdpglem1  35286  mapdindp0  35333  hlhilocv  35574  rntrclfvOAI  35579  ismrcd1  35586  ismrcd2  35587  coeq0i  35641  hbtlem6  36034  rgspnval  36080  iocinico  36142  trclubNEW  36272  wessf1ornlem  37513  iccdifprioo  37702  cncfuni  37850  cncfiooicclem1  37857  dvresntr  37874  dvmptresicc  37877  itgsubsticclem  37938  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem48  38119  fourierdlem49  38120  fourierdlem50  38121  qndenserrn  38269  prsal  38280  intsaluni  38289  sssalgen  38295  dfsalgen2  38301  sge0f1o  38327  sge0split  38354  ismeannd  38410  caragensspw  38438  caragendifcl  38443  carageniuncl  38452  caratheodorylem1  38455  hoicvrrex  38485  ovnssle  38490  ovn02  38497  ovnsubadd  38501  hoidmv1le  38523  ovnlecvr2  38539  ovncvr2  38540  isvonmbl  38567  vonmblss  38569  ovolval4lem2  38579  ovnovollem1  38585  ovnovollem2  38586  subsubmgm  40166
  Copyright terms: Public domain W3C validator