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

Theorem sseqtrd 3506
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 3498 . 2  |-  ( ph  ->  ( A  C_  B  <->  A 
C_  C ) )
41, 3mpbid 213 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3442
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 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  sseqtr4d  3507  uniintsn  4296  oeeui  7311  nnaword2  7339  oaabs2  7354  erssxp  7394  fipwuni  7946  ordtypelem7  8039  cantnflem3  8195  cdainf  8620  ficardun2  8631  ackbij1lem12  8659  ackbij1b  8667  fin1a2lem13  8840  winafp  9121  ioodisj  11760  reltrclfv  13060  prodss  13979  vdwlem11  14895  mrcssv  15462  mrcsscl  15468  mrcuni  15469  mressmrcd  15475  mreexexlem2d  15493  mreexexlem3d  15494  mreexfidimd  15498  subcss2  15690  resssetc  15929  funcsetcres2  15930  estrres  15966  poslubdg  16337  ipodrsfi  16351  acsmap2d  16367  mrelatlub  16374  mreclatBAD  16375  subsubm  16546  subsubg  16782  oppglsm  17220  subglsm  17249  lsmdisj  17257  gsumval3  17467  dprdres  17587  dprdss  17588  dprd2da  17601  dmdprdsplit2lem  17604  ablfac1b  17629  pgpfac1lem3  17636  issubdrg  17959  subsubrg  17960  islssd  18085  lspun  18136  lspssp  18137  lsslsp  18164  lsmssspx  18237  lspabs2  18269  lspabs3  18270  lspsolvlem  18291  lbsextlem3  18309  mplbas2  18620  gsumply1subr  18753  qsssubdrg  18953  obselocv  19213  lsslindf  19310  tgcl  19907  basgen  19926  tgfiss  19929  bastop1  19931  bastop2  19932  clsss2  20010  elcls3  20021  topssnei  20062  neiptopnei  20070  neitr  20118  restcls  20119  restlp  20121  ordtrest2  20142  iscncl  20207  cncls2  20211  cncls  20212  cnntr  20213  lmcls  20240  tgcmp  20338  cmpcld  20339  uncmp  20340  hauscmplem  20343  cmpfi  20345  clscon  20367  2ndcsb  20386  2ndcctbss  20392  2ndcomap  20395  nllyrest  20423  1stckgenlem  20490  kgencn2  20494  kgen2cn  20496  ptbasfi  20518  txcld  20540  txcls  20541  txbasval  20543  neitx  20544  ptcld  20550  ptclsg  20552  txnlly  20574  hausdiag  20582  txkgen  20589  xkopt  20592  xkopjcn  20593  xkococnlem  20596  cnmpt1res  20613  cnmpt2res  20614  imasnopn  20627  imasncld  20628  imasncls  20629  qtopcld  20650  qtoprest  20654  qtopcmap  20656  kqcldsat  20670  kqreglem2  20679  kqnrmlem2  20681  hmeontr  20706  neifil  20817  fgtr  20827  trnei  20829  uffixfr  20860  uffix2  20861  uffixsn  20862  elflim  20908  flimclslem  20921  fclsopn  20951  fclscmpi  20966  fclscmp  20967  alexsubALTlem3  20986  alexsubALT  20988  ptcmplem3  20991  subgntr  21043  opnsubg  21044  clssubg  21045  clsnsg  21046  cldsubg  21047  tgpconcompeqg  21048  snclseqg  21052  tsmsgsum  21075  tsmsid  21076  tgptsmscld  21087  ustssco  21151  utop2nei  21187  utop3cls  21188  utopreg  21189  cnextucn  21240  ressprdsds  21308  lpbl  21440  met2ndci  21459  prdsxmslem2  21466  metustexhalf  21493  psmetutop  21504  tgioo  21716  metdstri  21770  metdseq0  21773  xlebnum  21880  clsocv  22105  metelcls  22158  cmetss  22168  relcmpcmet  22170  cmpcmet  22171  minveclem4a  22256  uniioovol  22404  uniioombllem3  22411  limcres  22709  dvbss  22724  perfdvf  22726  dvreslem  22732  dvres2lem  22733  dvcnp2  22742  dvaddbr  22760  dvmulbr  22761  dvcmulf  22767  dvcj  22772  dvnfre  22774  dvmptres2  22784  dvmptcmul  22786  dvmptntr  22793  dvlip2  22815  dvcnvrelem2  22838  ftc1cn  22863  taylfvallem1  23168  taylply2  23179  taylply  23180  dvtaylp  23181  dvntaylp  23182  dvntaylp0  23183  taylthlem1  23184  taylthlem2  23185  ulmdvlem3  23213  pserulm  23233  shsub2  26804  spanssoc  26828  shub2  26862  ococin  26887  ssjo  26926  chub2  26987  spanpr  27059  elnlfn  27407  mdslj1i  27798  mdslmd3i  27811  mdexchi  27814  chirredlem1  27869  atcvat3i  27875  mdsymlem1  27882  mdsymlem5  27886  imadifxp  28042  qtophaus  28493  locfinreflem  28497  fsumcvg4  28586  esum2d  28744  omsmon  28950  omssubadd  28952  carsggect  28970  carsgclctun  28973  sitgclg  28994  eulerpartlemgf  29029  cvmscld  29775  cvmliftmolem1  29783  cvmlift2lem9  29813  cvmlift2lem11  29815  cvmlift3lem6  29826  nodense  30354  opnregcld  30762  ivthALT  30767  neibastop2  30793  fnemeet1  30798  fnejoin1  30800  poimirlem11  31645  poimirlem12  31646  poimirlem30  31664  ftc1cnnc  31710  sstotbnd  31801  ssbnd  31814  heibor1lem  31835  heiborlem3  31839  heibor  31847  lsmsat  32273  lssats  32277  lcvexchlem3  32301  lsatcvat3  32317  lkrscss  32363  lkrpssN  32428  pmod1i  33112  pclbtwnN  33161  pclunN  33162  pclss2polN  33185  pcl0N  33186  sspmaplubN  33189  paddunN  33191  pnonsingN  33197  pclfinclN  33214  osumcllem4N  33223  dia2dimlem13  34343  dvhopellsm  34384  dvadiaN  34395  dicelval1stN  34455  dicelval2nd  34456  dihssxp  34519  dihvalrel  34546  dochsscl  34635  dihoml4  34644  dochnoncon  34658  dvh3dim3N  34716  lcfrlem2  34810  lcfrlem5  34813  lcfr  34852  lcdlsp  34888  mapdsn  34908  mapdlsm  34931  mapdpglem1  34939  mapdindp0  34986  hlhilocv  35227  rntrclfvOAI  35232  ismrcd1  35239  ismrcd2  35240  coeq0i  35294  hbtlem6  35684  rgspnval  35723  iocinico  35785  wessf1ornlem  37072  iccdifprioo  37192  cncfuni  37326  cncfiooicclem1  37333  dvresntr  37350  dvmptresicc  37353  itgsubsticclem  37411  fourierdlem42  37570  fourierdlem48  37576  fourierdlem49  37577  fourierdlem50  37578  prsal  37716  intsaluni  37725  sge0f1o  37748  sge0split  37775  ismeannd  37804  caragensspw  37829  caragendifcl  37834  carageniuncl  37843  caratheodorylem1  37846  subsubmgm  38545
  Copyright terms: Public domain W3C validator