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

Theorem sseqtrd 3983
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrd.1 (𝜑𝐴𝐵)
sseqtrd.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
sseqtrd (𝜑𝐴𝐶)

Proof of Theorem sseqtrd
StepHypRef Expression
1 sseqtrd.1 . 2 (𝜑𝐴𝐵)
2 sseqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32sseq2d 3975 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 231 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-in 3916  df-ss 3926
This theorem is referenced by:  sseqtrrd  3984  uniintsn  4947  fssdmd  6683  oeeui  8517  nnaword2  8545  oaabs2  8563  erssxp  8605  fipwuni  9296  cantnflem3  9561  ficardun2  10072  ficardun2OLD  10073  ackbij1lem12  10101  ackbij1b  10109  fin1a2lem13  10282  winafp  10567  ioodisj  13329  reltrclfv  14837  prodss  15766  mrcssv  17430  mrcsscl  17436  mrcuni  17437  mressmrcd  17443  mreexexlem2d  17461  mreexexlem3d  17462  mreexfidimd  17466  subcss2  17665  resssetc  17914  funcsetcres2  17915  estrres  17963  poslubdg  18239  ipodrsfi  18364  acsmap2d  18380  mrelatlub  18387  mreclatBAD  18388  subsubm  18563  subsubg  18886  trivsubgd  18890  trivnsgd  18909  oppglsm  19359  subglsm  19390  lsmdisj  19398  gsumval3  19619  dprdres  19742  dprdss  19743  dprd2da  19756  dmdprdsplit2lem  19759  ablfac1b  19784  pgpfac1lem3  19791  issubdrg  20176  subsubrg  20177  islssd  20325  lspun  20377  lspssp  20378  lsslsp  20405  lsmssspx  20478  lspabs2  20510  lspabs3  20511  lspsolvlem  20532  lbsextlem3  20550  qsssubdrg  20785  obselocv  21063  lsslindf  21165  mplbas2  21371  gsumply1subr  21533  tgcl  22247  basgen  22266  tgfiss  22269  bastop1  22271  bastop2  22272  clsss2  22351  elcls3  22362  topssnei  22403  neiptopnei  22411  neitr  22459  restcls  22460  restlp  22462  ordtrest2  22483  iscncl  22548  cncls2  22552  cncls  22553  cnntr  22554  lmcls  22581  tgcmp  22680  cmpcld  22681  uncmp  22682  hauscmplem  22685  cmpfi  22687  clsconn  22709  2ndcsb  22728  2ndcctbss  22734  2ndcomap  22737  nllyrest  22765  1stckgenlem  22832  kgencn2  22836  kgen2cn  22838  ptbasfi  22860  txcld  22882  txcls  22883  txbasval  22885  neitx  22886  ptcld  22892  ptclsg  22894  txnlly  22916  hausdiag  22924  txkgen  22931  xkopt  22934  xkopjcn  22935  xkococnlem  22938  cnmpt1res  22955  cnmpt2res  22956  imasnopn  22969  imasncld  22970  imasncls  22971  qtopcld  22992  qtoprest  22996  qtopcmap  22998  kqcldsat  23012  kqreglem2  23021  kqnrmlem2  23023  hmeontr  23048  neifil  23159  fgtr  23169  trnei  23171  uffixfr  23202  uffix2  23203  uffixsn  23204  elflim  23250  flimclslem  23263  fclsopn  23293  fclscmpi  23308  fclscmp  23309  alexsubALTlem3  23328  alexsubALT  23330  ptcmplem3  23333  subgntr  23386  opnsubg  23387  clssubg  23388  clsnsg  23389  cldsubg  23390  tgpconncompeqg  23391  snclseqg  23395  tsmsgsum  23418  tsmsid  23419  tgptsmscld  23430  ustssco  23494  utop2nei  23530  utop3cls  23531  utopreg  23532  cnextucn  23583  ressprdsds  23652  lpbl  23787  met2ndci  23806  prdsxmslem2  23813  metustexhalf  23840  psmetutop  23851  tgioo  24087  metdstri  24142  metdseq0  24145  xlebnum  24256  clsocv  24542  metelcls  24597  metsscmetcld  24607  cmetss  24608  relcmpcmet  24610  cmpcmet  24611  minveclem4a  24722  uniioovol  24871  uniioombllem3  24877  limcres  25178  dvbss  25193  perfdvf  25195  dvreslem  25201  dvres2lem  25202  dvmptresicc  25208  dvcnp2  25212  dvaddbr  25230  dvmulbr  25231  dvcmulf  25237  dvcj  25242  dvnfre  25244  dvmptres2  25254  dvmptcmul  25256  dvmptntr  25263  dvlip2  25287  dvcnvrelem2  25310  ftc1cn  25335  dvntaylp  25658  taylthlem1  25660  ulmdvlem3  25689  pserulm  25709  nodense  26968  shsub2  30072  spanssoc  30096  shub2  30130  ococin  30155  ssjo  30194  chub2  30255  spanpr  30327  elnlfn  30675  mdslj1i  31066  mdslmd3i  31079  mdexchi  31082  chirredlem1  31137  atcvat3i  31143  mdsymlem1  31150  mdsymlem5  31154  imadifxp  31323  fnpreimac  31391  suppovss  31400  symgcom2  31736  pmtrcnelor  31743  cycpmco2f1  31774  1fldgenq  31889  0ringidl  31998  elrspunidl  31999  0ringprmidl  32018  idlsrgmulrss1  32049  idlsrgmulrss2  32050  drgextlsp  32085  lvecdim0  32094  lbslsat  32103  dimkerim  32112  fedgmullem2  32115  fedgmul  32116  qtophaus  32197  locfinreflem  32201  rspecbas  32226  zarclssn  32234  zarmxt1  32241  zarcmplem  32242  fsumcvg4  32311  esum2d  32472  omsmon  32678  omssubadd  32680  carsgclctun  32701  sitgclg  32722  eulerpartlemgf  32759  reprpmtf1o  33019  cvmscld  33647  cvmliftmolem1  33655  cvmlift2lem9  33685  cvmlift2lem11  33687  cvmlift3lem6  33698  opnregcld  34733  ivthALT  34738  neibastop2  34764  fnemeet1  34769  fnejoin1  34771  pibt2  35819  poimirlem11  36020  poimirlem12  36021  poimirlem30  36039  ftc1cnnc  36081  sstotbnd  36165  ssbnd  36178  heibor1lem  36199  heiborlem3  36203  heibor  36211  lsmsat  37401  lssats  37405  lcvexchlem3  37429  lsatcvat3  37445  lkrscss  37491  lkrpssN  37556  pmod1i  38242  pclbtwnN  38291  pclunN  38292  pclss2polN  38315  pcl0N  38316  sspmaplubN  38319  paddunN  38321  pnonsingN  38327  pclfinclN  38344  osumcllem4N  38353  dia2dimlem13  39470  dvhopellsm  39511  dvadiaN  39522  dicelval1stN  39582  dicelval2nd  39583  dihssxp  39646  dihvalrel  39673  dochsscl  39762  dihoml4  39771  dochnoncon  39785  dvh3dim3N  39843  lcfrlem2  39937  lcfrlem5  39940  lcfr  39979  lcdlsp  40015  mapdsn  40035  mapdlsm  40058  mapdpglem1  40066  mapdindp0  40113  hlhilocv  40355  rntrclfvOAI  40916  ismrcd1  40923  ismrcd2  40924  coeq0i  40978  hbtlem6  41358  rgspnval  41397  iocinico  41448  omabs2  41459  trclubNEW  41690  ntrk2imkb  42110  isotone1  42121  k0004ss3  42226  iccdifprioo  43545  limsupequzmptlem  43760  cncfuni  43918  cncfiooicclem1  43925  dvresntr  43950  itgsubsticclem  44007  fourierdlem42  44181  fourierdlem48  44186  fourierdlem49  44187  fourierdlem50  44188  qndenserrn  44331  prsal  44350  intsaluni  44361  sssalgen  44367  dfsalgen2  44373  sge0split  44441  ismeannd  44499  caragensspw  44541  caragendifcl  44546  carageniuncl  44555  caratheodorylem1  44558  hoicvrrex  44588  ovnssle  44593  ovn02  44600  ovnsubadd  44604  hoidmv1le  44626  ovnlecvr2  44642  ovncvr2  44643  isvonmbl  44670  vonmblss  44672  ovolval4lem2  44682  ovnovollem1  44688  ovnovollem2  44689  incsmf  44774  decsmf  44799  uspgropssxp  45837  subsubmgm  45882  mreuniss  46723  restcls2lem  46736  restcls2  46737  cnneiima  46740
  Copyright terms: Public domain W3C validator